Функциональная чистота

Замыкания? Нет, не слышал.

В /c/ свали с такой толстотой.

f1 и f2 — это разные функции. Чистые, да.

Возвращает ли внутренняя ф-ця /y.x (она же - f1 и f2) одинаковые значения при одинаковых аргументах?

Да. При любом значении y, это функция вернёт значение свободной переменной x.

И что? Замыкания должны изменять св-ва функций?

это функция вернёт значение свободной переменной x

В любом ЯП, в тч не чистом, ф-ция вернет значение свободной переменной x, каким бы оно ни было.

Тащемта, от этого функция чистой быть не перестаёт.

А в чем же тогда смысл чистоты языка?

Замыкания должны изменять св-ва функций?

С чего это они изменяют свойства функций?

 — Является ли внутренняя функция /y.x функцией?

Нет, потому что терм незамкнут. А ты - долбоеб.

В ссылочной прозрачности.

Ты онанист, объясни-ка тогда, чем является функция внутри незамкнутого терма? Может фалоимитатором, который у тебя изо рта торчит?

Ты онанист, объясни-ка тогда, чем является функция внутри незамкнутого терма?

Ничем не является. И функцией она не является. Не надо так ее называть. Чем-то может являться только нормализуемый терм, незамкнутый терм по определению ненормализуем.

Блестящяя расстановка точек над Ы.

Тогда откуда (концептуально) берется ф-я записанная в f1 b f2? Она что из воздуха вырастает? Мне казалось, как-раз (да и пишут об этом обычно), что она возвращается как-раз из ф-ции, на то они и ф-ции высших порядков. Ведь это обычно звучит, как «ф-ция возвращает ф-цию в качестве значения». Так что-же незамкнутый терм на самом деле возвращает? Синтаксическую конструкцию, которая лишь потом становиться ф-цией? В какой момент она ей становиться? На каком этапе редукций?

Покажи мне /c/.

Тогда откуда (концептуально) берется ф-я записанная в f1 b f2? Она что из воздуха вырастает?

в f1 лежит функция (/x./y.x 1), в f2 - (/x./y.x 1). Терму /y.x никакой функции не соответствует.

Так что-же незамкнутый терм на самом деле возвращает?

Незамкнутый терм ничего не возвращает и ничего не принимает. Незамкнутый терм вообще никакому объекту не соответствует и смысла не имеет.

Синтаксическую конструкцию, которая лишь потом становиться ф-цией? В какой момент она ей становиться?

Никто ничем никогда не становится. терм /y.x как ф-ей не был так никогда ей и не станет. ф-ми являются, например, терм /x./y.x, терм (/x./y.x 1) и бета-эквивалентный ему терм /y.1.

все, что в ОП написано, вообще никак с языками программирования не связано - это чистый матан^Wлямбда-исчисление

Или, объясню иначе: когда мы говорим, что «данный терм обозначает такой-то объект», то имеется ввиду, что при вычислении этого терма мы ровно этот объект и получим. Например, при вычислении (\x y.x) 1 мы получим \y.1, что есть константная ф-я, значит (\x y.x) 1. обозначает константную ф-ю, как и /y.1. При вычислении виснущего (ненормализуемого) терма мы ничего не получим => виснущий терм ничего не значит. Так же мы ничего не получим при вычислении незамкнутого терма => он ничего не значит.

никак с языками программирования не связано - это чистый матан^Wлямбда-исчисление

Но ведь все проповедники ФП постоянно жужжат, что ФП основано на LC.

-- Является ли внутренняя функция /y.x функцией?

Нет.

f1 = parent 1 = (\x. \y. x) 1 = \y. 1
f2 = parent 2 = (\x. \y. x) 2 = \y. 2

Толсто.

Но ведь все проповедники ФП постоянно жужжат, что ФП основано на LC

наверное, так оно и есть.

но я о том, что постановка вопроса на термины фп никак не опирается, только на термины математики.

ошибка чисто логическая, начинается отсюда:

 — Является ли функция f1 внутренней ф-цией /y.x?

 — Да.

на самом деле, нет. f1 = /y.1, а f2=/y.2

f1=/y.x - это вообще некорректная запись, т.к. x - хз что

Терм /y.x является ф-цией? Если это не функция, то что тогда? Как обозвать?

Если это не функция, то что тогда? Как обозвать?

Незамкнутое лямбда-выражение.

Термы не могут являться чем-либо, они могут что-то обозначать. Либо не обозначать, если бессмысленны. В модели лямбда-исчисления термам сопоставляются ф-и и только они, соответственно терм может либо обозначать ф-ю, либо обозначать ничего. нормализуемые термы обозначают ф-и, ненормализуемые термы (в том числе незамкнутые) ничего не обозначают.

f1=/y.x - это вообще некорректная запись, т.к. x - хз что

Неправда, так в LC как раз определяется false. Без этого выражения LC вообще рухнет, Вы пытаетесь разрушить самые что ни на есть основы:)

нафига в LC false?

false определяется как /x y.y, не надо врать

Что бы как то выражать ветвления. А нафига тогда LC, если оно не несет никакой семантики? Выражения должны что-то выражать, не так ли?

Никак. Некорректная конструкция.

В лямбда-исчислении нет =, его используют что бы не писать одно и тоже много раз, это просто синоним. Правая часть синоним левой.

с языками программирования не связано

лямбда-исчисление

/ 0

вы (буэ)

1) почему-то решили, что \a.b и \a.b.b - это одно и то же

2) почему-то решили, что \a.a.b и \a.b.b - единственный способ задать булево поле на лямбдах

3) почему-то решили, что один пример использования LC является его основой

Проспись.

еще раз, для слабозрячих: лямбда-исчисление это математика, не программирование.

Всюду пишется, что LC - это ЯП

машина тьюринга - тоже яп. только это все равно чисто математическая, непротиворечивая уже поэтому, структура

Нет.

Да. Вот код на хаскеле (в LC так же)

f1 = const 1
f2 = const 2
t1 = f1 () -- => 1
t2 = f2 () -- => 2

TC во всём прав, только он на последний вопрос не ответил, чтобы на него ответить, нужно сказать, что const 1 и const 2 возвращают разные функции — не проблема, аргументы-то разные, f1 != f2, то что разные функции при одинаковых аргументах могут возвращать разные значения никого не должно удивлять, позволю себе </thread>

Дальше можно продолжать тупить или обсудить ещё что-нибудь :)

Ты писал не о программировании, а о языках программирования.

Теперь define математика. Вангую, они относятся именно к ней.

чисто математическая, непротиворечивая уже поэтому

Что за феерический бред. LC протеворечиво, это доказано.

пруф

Адепты ФП утверждают, что правильное определение ФП это «программирование с помощью математических функций», то есть LC — чистое, типизированное или нет. Вообще, грязного LC по идее нет, иначе как все её (теории) равенства будут выполняться.

Всюду пишется, что LC - это ЯП

Что за бред, где это «всюду»? По-моему, лямбда-исчисление появилось за годы до первого ЯП. Это попытка формализации понятия вычисления, а уж то, что некоторые ЯП по определенным причинам используют его для формализации программ, на них написанных - дело совсем десятое.

LC протеворечиво, это доказано

4.2, доказано как раз обратное.

ок, s/никак не связано/не зависит от/

Э, что? У меня нет в телефоне ghci. Но...

ghci> let f = \y -> x
???

4.2

Я читал это у Скотта, что-то о решетках, сейчас пруф не найду, но это есть в инете. Там это было сказано в контексте того, что Черч пытался доказать непротиворечивость теории Фреге, но обосрался, подробностей не помню.

где это «всюду»

Всюду, значит всюду. Учи матчасть, я 2Х2 доказывать не собираюсь. Еще раз LC — это ЯП (по общепризнаному мнению).

теории Фреге

я не в курсе, что это, но почему недоказанность непротиворечивости должна означать противоречивость?

Кукаретик, ты?

спор о терминологии бесполезен. можно навыдумывать сколько угодно абсолютно эквивалентных определений LC

k :: b -> (a -> b)
k = \x -> \_ -> x
-- k = \x -> \y -> x
-- k = \x _ -> x
-- k x = \y -> x
-- k x = \_ -> x
-- k x _ = x

f1 :: a -> Bool
f1 = k True
-- => some function, i.e. \_ -> True

f2 :: a -> Bool
f2 = k False
-- => another (!) function, i.e. \_ -> False
-- f1 /= f2 (!)

t1 :: Bool
t1 = f1 ()
-- => True

t2 :: Bool
t2 = f2 ()
-- => False

k n возвращает замыкание \y -> x в котором x связан c переданным n (лежит в данных замыкания, как обычно).