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

Емнип, там доказана протеворечивость. А теория Фреге (о которой речь), была попыткой снять парадокс Рассела. Но подробности я не помню.

TC во всём прав

Да-да, особенно когда говорит, что ((\x y -> x) 1) — то же самое, что (\y -> x).

а как парадокс Рассела связан с LC?

теория Фреге

кинь ссылку на формулировку

Ну да. В чем проблема?

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

Нет. Так же как \_ -> x.

Все дальнейшее рассуждение ОПа построено на внезапном изменении x. То есть он не считал x константой.

Вот это.

Щас попробую найти, пока, даю цитату с википедии

Парадокс Рассела (иногда парадокс Рассела-Цермело) — открытый в 1901 году[1] Бертраном Расселом и позднее независимо переоткрытый Э. Цермело теоретико-множественный парадокс, демонстрирующий противоречивость логической системы Фреге, являвшейся ранней попыткой формализации наивной теории множеств Г. Кантора.

Может ты быстрей найдешь. Я давно читал, толком не помню.

что такое парадокс Рассела, я знаю. я не пойму, как он с LC связан

не знаю, что такое теория френе. если речь про т.н. треугольник его имени - то тоже не ясно, где связь с LC

где связь с LC

Я же сказал, что (может я ошибаюсь), когда то листал книжку Скотта о решетках, и наткнулся там на его фразу о том, что теория черча была попыткой доказать теорию фреге, но провальной попыткой. Это все, что я помню, а источник не могу найти. Если найду, отпишусь.

Ты что-то не так запомнил.

Скотт сам первый (с точки зрения построения модели, так-то есть теорема Чёрча-Розера) и доказал непротиворечивость нетипизированного лямбда-исчисления. Более ранние результаты Клини и Розера говорят о противоречивости нетипизированного варианта как логической системы — функтора из категории ULC в логически «хорошую» категорию нет, но как теория ULC непротиворечива — равенства различимы как теоремы и у теории есть модель в которых они реализуются.

Типизированные варианты тем более непротиворечивы, уже в т.ч. и логически — функтор есть, известен как изоморфизм Карри-Говарда.

http://en.wikipedia.org/wiki/Lambda_calculus#Lambda_calculus_in_history_of_ma...

http://plato.stanford.edu/entries/lambda-calculus/#ConLCal

http://plato.stanford.edu/entries/lambda-calculus/#SemLCal

http://arxiv.org/abs/0904.4756

http://mathoverflow.net/q/16752

http://turing100.acm.org/lambda_calculus_timeline.pdf

http://en.wikipedia.org/wiki/Model_theory#Using_the_compactness_and_completen...

http://en.wikipedia.org/wiki/Curry–Howard_correspondence

а как парадокс Рассела связан с LC?

Ну, его можно закодировать в LC (АКА «парадокс Клини-Розье») и получить выражение без бета-эта нормальной формы. Не очень силен в истории и теории множеств — наверное, на тот момент это было очень символично. Но Чёрч точно потом сооружал свое типизированное лямбда исчисление, чтобы парадокса избежать.

Нет.

Является, конечно, это замыкание. k True возвращает эту внутреннюю функцию \_ -> True, k Fasle — \_ -> False.

Ошибка только ближе к концу, в отождествлении f1 и f2, тогда как это разные замыкания — одна от k _True_, другая — от k _False_.

/y.x (она же - f1 и f2)

Ну да, последний вопрос у него twisted. Но всему остальному ещё можно придать смысл :)

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

In mathematics, the Kleene–Rosser paradox is a paradox that shows that certain systems of formal logic are inconsistent, in particular the version of Curry's combinatory logic introduced in 1930, and Church's original lambda calculus, introduced in 1932–1933, both originally intended as systems of formal logic. The paradox was exhibited by Stephen Kleene and J. B. Rosser in 1935.

http://en.wikipedia.org/wiki/Kleene–Rosser_paradox

Да.

Ты меня разочаровываешь. Если \y.x - функция, то какая? Возьмем обычную ULC с семантикой Скотта.

Я про то что внутренний терм \y -> x является результатом вызова k n и, очевидно, представляет собой функцию (вложенные «функции»/замыкания в ЯП) \_ -> n ((\y -> x)[x -> n]).

Сам голый терм \_ -> x функцию не представляет, конечно.

Это противоречивость ULC при попытке её использовать как логическую систему, как теория она может быть непротиворечива. Типизированные варианты непротиворечивы как теории и как логические системы.

интересно, хотя не понятно: парадокс клини-россера рекурсивный, хотя LC не позволяет использовать рекурсию напрямую.

языки типа Haskell, которые позволяют, страдают специальным значением undefined

соответственно, выражения типа x -> (x => False) в терминах хаскеля сводятся к undefined, в терминах машины тьюринга невычислимы, а в терминах LC некорректны, т.е. просто не несут смысла и не рассматриваются

and Church's original lambda calculus

возможно, «original LC» претерпело какие-то изменения с тех пор, и LC, которое сейчас называют LC, содержит соответствующие корректировки, сводящие парадокс на нет

Интересно получается. Значит, ф-ция, возвращенная из замыкания — это не ф-ция, до тех пор, пока она не возвращена, так чтоли получается? Где же тогда ФВП? Функция не может взять функцию как аргумент и возвратить ее же, в качестве значения?

точняк, противоречие - в самой логике, а не в LC // not sarcasm

хотя LC не позволяет использовать рекурсию напрямую.

А как же Y-комбинатор?

точняк, противоречие - в самой логике, а не в LC

Ну, это уже просто улет!:) А каким еще может быть противоречие, если не логическим?

Сам голый терм \_ -> x функцию не представляет, конечно.

а вот у опа представляет

LC

Нет такой вещи. Если говорим про нетипизированный вариант — говорим про него, нет там противоречий, как и в самой логике.

Значит, ф-ция, возвращенная из замыкания

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

как и в самой логике.

В логике нет противоречий? Пруф?

под противоречием в логике, в данном случае, понимаю конкретно парадокс рассела.

quasimoto, ^^

А какое формальное определение у «противоречиво как логическая система»? То есть у нас категория ULC, модели - функторы в Set, какой функтор должен быть, чтобы считаться функтором в «логическую систему» (и отсутствие которого будет трактоваться как «противоречивость в качестве логической системы»)?

логика высказываний и лпп непротиворечивы. открыт вопрос противоречивости арифметики и содержащих ее теорий, которые являются расширениями ЛПП.

А как же Y-комбинатор?

попробуй расписать x -> (x => False) через него.

тут выше подсказывали, что true = \a.b.a, false = \a.b.b

вангую, что X окажется не равен ни тому, ни другому

Значит, ф-ция, возвращенная из замыкания — это не ф-ция, до тех пор, пока она не возвращена, так чтоли получается?

Замыкание это сама возвращаемая функция, а не возвращающая.

Вложенный лямбда-терм (не говорю «функция») представляющий замыкание использует переменные которые в нём не замкнуты, сам по себе он математическую (!) функцию не представляет и в хаскелях просто не сконпелируется вне контекста функции которая его возвращает. Ну а так функция возвращающая замыкание имеет сигнатуру типа A -> Endo(A), очевидно, что она может при вызове с неким (x : A) вернуть некую (\y -> E[x, y]) : Endo(A).

Где же тогда ФВП?

В экспоненциалах :)

Функция не может взять функцию как аргумент и возвратить ее же, в качестве значения?

Может, только тут нет замыканий.

открыт вопрос противоречивости арифметики и содержащих ее теорий

А почему открыт? Я где-то читал, что ее противоречивость уже давно доказна, в том числе и Черчем.

Две разные функции возвращают разные значения для разных аргументов. Эка невидаль!

интересно, хотя не понятно: парадокс клини-россера рекурсивный

Он, конечно, рекурсивный — это ведь использование (Y NEG) самому к себе, где Y — игрек-комбинатор, а NEG f x y = f y x.

LC не позволяет использовать рекурсию напрямую

Речь о нетипизированном LC. Там нет сильной нормализации.

В логике нет противоречий? Пруф?

В любой непротиворечивой теории нет противоречий, очевидно. Как принято доказывать, что некая теория непротиворечива? Например, выше я уже приводил ссылку — http://en.wikipedia.org/wiki/Model_theory#Using_the_compactness_and_completen....

Считаем теорию «логикой» если она годится для построения логических рассуждений, то есть там есть типичные ингредиенты _|_, T, => и т.п. и они взаимопереводимы с этими же утверждениями какой-нибудь тестовой «логики» (по желанию).

Про понятие непротиворечивости в лямбда-исчислении тоже была ссылка — http://plato.stanford.edu/entries/lambda-calculus/#ConLCal. И про модели тоже — http://plato.stanford.edu/entries/lambda-calculus/#SemLCal, http://arxiv.org/abs/0904.4756.

В нетипизированном варианте просто не нужно переводить/интерпретировать термы как логические утверждения, иначе можно получить парадоксы именно в рамках теории ULC. Тестовая непротиворечивая «логика» или метатеория (раз уж мы её используем) не перестают быть непротиворечивыми.

Я где-то читал, что ее противоречивость уже давно доказна, в том числе и Черчем.

Непротиворечивость PA доказана Гентзелем, просто не всем нравится это доказательство.

Непротиворечивость арифметики Пресбургера доказана.

Можно построить вариант арифметики способный доказать свою собственную непротиворечивость.

В любой непротиворечивой теории

Это та, которая неполна?

А почему открыт? Я где-то читал, что ее противоречивость уже давно доказна, в том числе и Черчем.

Эта непротиворечивость доказана методами некоторой более содержательной теории, непротиворечивость которой, опять-таки, можно доказать лишь методами более содержательной теории и т.д.

Можно построить вариант арифметики способный доказать свою собственную непротиворечивость.

Например:

def "вариант арифметики" 
body:
axiom1 "я непротеворечива"
axiom2: "если вылезает противоречие, например, парадокс лжеца, см пункт 3" 
axiom3: "выражения, допускающие парадоксы запрещены"

Непротиворечивость арифметики Пресбургера доказана.

Ну она слабее обычной.

Считаем теорию «логикой» если она годится для построения логических рассуждений, то есть там есть типичные ингредиенты _|_, T, => и т.п. и они взаимопереводимы с этими же утверждениями какой-нибудь тестовой «логики» (по желанию).

Но у нас в Set нету никаких «_|_, T, => и т.п.». Можно все-таки формальное определение, что значит «противоречива в качестве логики»? Что вообще такое «рассматривать теорию в качестве логической системы»? Опять же - это ведь отношение между теориямИ, но речь-то о моделях?

Эта непротиворечивость доказана

Я сказал противоречиость.

В нетипизированном варианте просто не нужно переводить/интерпретировать термы как логические утверждения

Как это вообще можно сделать, если «утверждения - это типы», а типов в ULC нет?

А противоречивость-то с какого доказана? Если арифметика противоречива, то тогда всю математику можно выкидывать.

Можно построить вариант арифметики способный доказать свою собственную непротиворечивость.

ИМХО, логическая система, которая может делать суждения о самой себе и собственной непротиворечивости, по определению противоречива, это сродни парадоксу Расселла. Получается, что в рамках своей аксиоматики она должна доказать свою асиоматику, опираясь на теоремы, определяемые этой же самой аксиоматикой.

Это та, которая неполна?

Необязательно, может быть полна.

Например

http://www.cs.albany.edu/~dew/m/jsl1.pdf

axiom1

theoreme.

Если арифметика противоречива, то тогда всю математику можно выкидывать.

Это проблемы тех, кто ей пользуется. ожешь выкинуть, если хочешь.

Необязательно, может быть полна.

Как же это согласуется с теоремой Геделя о неполноте?

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

 — Да.

Нет.

ИМХО, логическая система, которая может делать суждения о самой себе и собственной непротиворечивости

Нет.

Это проблемы тех, кто ей пользуется. ожешь выкинуть, если хочешь.

Ей много кто пользуется.Но, к счастью, никто пока непротиворечивость не показал.