почему лямбда-калкулюс нельзя смоделировать в виде функций на множествах

[juan_gandhi]

Лямбда-калкулюс состоит из термов, каковые бывают или переменными (x, y, z), или абстракциями (λv.M, где v - переменная, а M - терм), или аппликациями, (M N, где M и N - термы).
Например, λf.(λx.f(xx))(λx.f(xx))
В первой половине 20-го века народ ломал головы - ну а как же это выразить в теории множеств-то?
Ну вроде бы речь идет о функциях. Ну пусть каждая переменная обозначает функцию, и каждое выражение обозначает функцию (где свободные переменные - под лямбдой).
Ну и вообразим на минутку, что мы лямбда-калкулюс моделируем в теории множеств, и каждый лямбда-терм M моделируется функцией f_M. Тогда терм M M будет моделироваться значением f_M(f_M). Это мы функцию применяем к самой себе. Ну чо, на языках программирования можно же.
Но штука такая, что в теории множеств, кроме множеств, ничего нету. Так что f_M - это какое-то множество, а т.к. оно у нас функция, то это множество пар. И раз она применима к самой себе, то компонентой одной из таких пар является сама f_M.
И что теперь? Пары в теории множеств моделируются как множества, (a,b) = {{a}, {a,b}}. Так что у нас получается, что f_M ∈ (f_M, ?) ∈ f_M. Вы видим цепочку, где множество является элементом элемента самого себя. Такие множества называются Квайнами, и они запрещены в приличных теориях множеств (Цермело-Френкеля, например). Ну и все, фокус не удался. В частности, не удался и фокус смоделировать язык программирования в теории множеств с помощью просто функций.
Не, на самом деле, смоделировать потом таки удалось - когда Дана Скотт придумал топологию Скотта. Короче, все не так-то просто в нашем дискурсе.
Есть вопросы?

Comments

[chaource]

Вопросы еще по поводу типизированнаго лямбда-калькулюса, тамъ нельзя f(f). Это значитъ, тамъ возможны модели на обычныхъ множествахъ?

[juan_gandhi]

Мне кажется, что да - Sets же декартово-замкнутая категория. Это, по-моему, покрыто в маленькой зеленой книжке Пирса ("категории для учоных, или что-то такое).

[pappadeux]

для компутерных учоных

[http://users.livejournal.com/sorcerer-/]

О, отлично! Формальное доказательство, что тайпскрипт - не суперсет джаваскрипта, а вообще - хуже чем сабсет.
Что я всегда эмпирически знал, но теперь есть чем тайпскрипт-фашистов троллить. Лол

[juan_gandhi]

Ну да. Вообще интересная тема, я не знаю ответа - моделирование нетипизированной лямбды в типизированной. Надо Барендрегта, э... перечитывать. Там эти темы должны быть раскрыты. Лямбды же разные бывают. И типизированных больше чем одна (Карри и Черча).

[juan_gandhi]

А, еще не будем забывать, что типизированных лямбд как минимум две, Черча и Карри.

[dmm]

For the simply typed lambda calculus, yes.

But for the polymorphic version, John Reynolds established in 1984 paper "Polymorphism is not set-theoretic" that the standard set-theoretic model of the ordinary typed lambda calculus cannot be extended to model the polymorphic version: https://hal.inria.fr/inria-00076261/document

Basically, there is a different domain equation instead of "D isomorphic to [D->D]" for the uptyped case, which must be satisfied for the polymorphic case.

In the polymorphic typed case, the required isomorphism is "D isomorphic to [[D->B]->B]", where B is some type containing more than one element. (See pages 4-5, and 11 of the paper, that is pages 7-8, and 14 of the PDF file.)

[dmm]

This is the author: https://en.wikipedia.org/wiki/John_C._Reynolds

[chaource]

It is unfortunately quite difficult for me to understand the Reynolds paper. I tried several times in the past, but gave up.

To me, an isomorphism between D and (D -> B) -> B does not seem to be a problem for a set-theoretic model. I do not really understand the arguments of Reynolds in that paper.


Is it again the argument about a circular membership chain? That D must be an element of some set, which is an element of another set, which is an element of D?


The argument based on power counting does not apply to computing, because not all functions can be programmed as lambda terms. The type D -> B, for example, is not modeled by the set of all functions between the sets D and B, but by the set of only those functions that correspond to some lambda-terms of the type D -> B.

Since lambda-terms are made up of finitely many symbols from a fixed finite alphabet, the set of all possible lambda-terms is no more than a countably infinite set.

So, the type D -> B is modeled by at most a countably infinite set of functions. Similarly for the type (D -> B) -> B.

[dmm]

Of course, the above result is about "system F". In some sense, that system is too powerful, as its type inference is not computable: https://en.wikipedia.org/wiki/System_F#Use_in_programming_languages

I don't know what is the status of this question for something like https://en.wikipedia.org/wiki/Hindley%E2%80%93Milner_type_system

[sassa_nf]

> (a,b) = {{a}, {a,b}}

Does this mean B→⊥ = id_B?

B→⊥ = {{b},{b,}} = {{b}}

id_B = {{b},{b,b}} = {{b},{b}} = {{b}}

[soid]

⊥ это пустое множество или какой-то другой зверек?

[juan_gandhi]

What is B→⊥ ? (if you mean ⊥ to be a singleton set, then no).

[juan_gandhi]

B→⊥ = ⊥, if you represent it in sets.

[soid]

Супер! Получается, математики поклоняясь богу ZFC приносят в жертву всю силу Черча-Тюринга, взамен получают заговор от порчи парадоксов Рассела, но при этом, все так же не могут ответить на главный вопрос – undecidability – не могут так же, как и компьютерщики, полюбившие свободу Тюринга от сексуальных предубеждений, и всю жизнь ковыряющие баги и никогда не знающие чего еще ожидать от их грешно зачатого кода?

[juan_gandhi]

ZFC годится для многих различных рассуждений, но многие эти рассуждения относятся к чему-то невычислимому. Что тоже ничего, но надо понимать, что оно невычислимо. Причем, на этой невычислимой математике построена теоретическая физика.

Да, впрочем, я недостаточно компетентен рассуждать на эти темы.

[sab123]

Что мешает взять такое-же-но-другое множество?

[juan_gandhi]

В смысле, одно и то же множество M будет вдруг другим? Или... что значит, "такое-же-но-другое"? Это теория множеств, там если все элементы одинаковы, то множества равны.

мы академиев не кончали

[dedekha]

поэтому просто вопрос к знающим людям - лямбда в лиспе и лямбда Черча это как-то связано с друг другом?

и еще один есть какие-то практические применения у всей этой монадистики?

Re: мы академиев не кончали

[juan_gandhi]

Монад там нету, а лисп просто является имплементацией лямбда-калкулюса.

Re: мы академиев не кончали

[chaource]

Вотъ вы скажите мнѣ... Это народу зачѣмъ-либо нужно? (Левъ Толстой)

Есть большая область примѣненiя у "монадистики" и лямбды, въ практическомъ функцiональномъ программированiи. Я зарабатываю себѣ на жизнь тѣмъ, что знаю, какъ и гдѣ это все примѣняется.

Одновременно, есть большое количество статей и книгъ о теорiи лямбда-калькулюса, лямбда въ стилѣ Черча, въ стилѣ Карри, теорiя моделей, теорiя доменовъ Скотта и т.д. У меня создалось впечатленiе, что почти все, написанное тамъ, на практикѣ не нужно. Но я буду очень радъ ошибиться.

[chaource]

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


Просто надо, чтобы всегда всѣ типы соотвѣтствовали другъ другу, и чтобы никогда никакое значенiе не могло быть неправильнаго типа. Чтобы всѣмъ функцiямъ было съ типами хорошо, и никакимъ не было дурно.

http://www.world-art.ru/lyric/lyric.php?id=18580

...буду говорить только о науке ... Что такое наука? Наука ... есть ... знание того, ... что точно хорошо всегда и везде и всем людям и что точно дурно всегда и везде и всем людям, т.е. знать, что должно и чего не должно делать. В этом, и только в этом, всегда и была и продолжает быть истинная, настоящая наука.
Наука эта есть действительная наука, т.е. собрание знаний, которые не могут сами собой открыться человеку и которым надо учиться и которым учился и весь род человеческий.

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

... главная основа науки та, из которой каждый человек может вывести ответы на все вопросы жизни, и коротка и проста и доступна всякому, как самому ученому, так и самому неученому человеку.

... не могло быть того, что мог бы узнать всякую нужную для блага всякого человека науку только тот, кому не нужно самому кормиться, а кто может на чужие труды 12 лет учиться в разных учебных заведениях. Не могло быть этого, и нет этого: настоящая наука та, которую необходимо знать каждому, доступна и понятна
каждому ...

Такова истинная наука, но не такова та наука, которая в наше время в
христианском мире считается и называется наукой. Наукой в наше время
считается и называется, как ни странно это сказать, знание всего, всего
на свете, кроме того одного, что нужно знать каждому человеку для того,
чтобы жить хорошей жизнью.
Люди, занимающиеся теперь наукой и считающиеся учеными, изучают все на
свете. И таких изучений, называемых наукой, такое огромное количество, что
едва ли есть на свете такой человек, который не то чтобы знал все эти так
называемые науки, но мог бы хотя перечислить их. Наук этих пропасть, с
каждым днем появляются новые. И все эти науки, называемые самыми странными
выдуманными греческими и латинскими словами, считаются одинаково важными и
нужными, так что нет никакого указания на то, какие из этих наук должны
считаться более, какие менее важными и какие поэтому должны изучаться прежде
и какие после, какие более и какие менее нужны людям.
Не только нет такого указания, но люди, верующие в науку, до такой степени
верят в нее, что не только не смущаются тем, что наука их не нужна, но,
напротив, говорят, что самые важные и полезные науки - это те, которые не
имеют никакого приложения к жизни, т.е. совершенно бесполезны. В этом, по их
понятиям, вернейший признак значительности науки.
Понятно, что людям, так понимающим науку, все одинаково нужно. Они с
одинаковым старанием и важностью исследуют вопрос о том, сколько Солнце
весит и не сойдется ли оно с такой или такой звездой, и какие козявки где
живут и как разводятся, и что от них может сделаться, и как Земля сделалась
Землею, и как стали расти на ней травы, и какие на Земле есть звери, и
птицы, и рыбы, и какие были прежде, и какой царь с каким воевал и на ком был
женат, и кто когда какие складывал стихи и песни и сказки, и какие законы
нужны, и почему нужны тюрьмы и виселицы, и как и чем заменить их, и из
какого состава какие камни и какие металлы, и как и какие пары бывают и как
остывают, и почему одна христианская церковная религия истинна, и как делать
электрические двигатели и аэропланы и подводные лодки, и пр. и пр. и пр. И
все это науки с самыми странными вычурными названиями, и всем этим с
величайшей важностью передаваемым друг другу исследованиям конца нет и не
может быть, потому что делу бывает начало и конец, а пустякам не может быть
и нет конца. Не может быть конца, особенно когда занимаются этими, так
называемыми науками люди, которые не сами кормятся, а которых кормят другие
и которым поэтому от скуки больше и делать нечего, как заниматься какими бы
то ни было забавами. Выдумывают эти люди всякие игры, гулянья, зрелища,
театры, борьбы, ристалища, в том числе и то, что они называют наукой.

[juan_gandhi]

Бурные, продолжительные аплодисменты. И это он еще теорию относительности не застал.

[chaource]

Но вообще-то уважуха автору сего блога. Знатный срачъ на 70+ комментарiевъ, послѣ какого-то достаточно заумнаго вопроса о лямбдахъ!

[juan_gandhi]

Ценная публика собралась.