Базовые концепты computer science на примере λ-исчисления

[_hum_]

Поскольку λ-исчисление минимально по форме, то, по логике, на его примере должна быть наиболее хорошо видна суть того или иного базового понятия из computer science. Вот, пока что удалось разглядеть:

1) значение < - > всякий λ-терм в нормальной форме (относительно βη-редукции), например, $\lambda f.\lambda x.x := 0$, $\lambda f.\lambda x.fx:= 1$;
2) выражение <-> всякий λ-терм;
3) вычисление выражения <-> алгоритмический процесс нормализации;
4) аппликативная/нормальная стратегия вычисления <-> вычисления с аппликативным/нормальным порядком редукции;
5) программа/исходные данные программы <-> λ-терм/значение к которому он будет применяться;
6) декларирование (связывание некоторого идентификатора x с некоторым объектом) <-> констатация по терму вида $(\lambda x.P)V$ того факта, что в терме $P$ при β-редукции вхождения связанной переменной $x$ будут замещаться связанным с ней (декларацией) термом $V$;
Пример. Конструкцию $(\lambda a.(\lambda x.ax))1$ можно воспринимать как аналог $ \mathrm{let}\, a = 1\,\mathrm{in}\, \lambda x.ax$

7) передача аргумента по значению <-> бета редукция с предварительной редукцией "аргумента" (то, к чему применяется абстракция) к нормальной форме;
8) передача аргумента по имени <-> бета редукция без предварительной редукции аргумента к нормальной форме;
9) статическое (лексическое) связывание <-> требование "неприкосновенности деклараций" при β-редукции, что выражается в требовании особым образом осуществлять подстановку, разводя путем α-редукции пересекающиеся имена переменных, если это может привести к изменению их декларативной связи с объектом.
Пример. С точки зрения λ-исчисления корректна такая последовательность редукций

$$(\lambda a.(\lambda x.(\lambda a.xa)0)a)1\,\, \rightarrow\,\, (\lambda a.(\lambda x.(\lambda a'.xa')0)a)1 \,\,\rightarrow\,\, (\lambda a.(\lambda a'.aa')0)1,$$

то есть,

$$\mathrm{let}\, a=1\, \mathrm{in}\, (\lambda x.(\mathrm{let}\, a = 0\, \mathrm{in}\, xa))a\,\, \rightarrow\,\, \mathrm{let}\, a=1\, \mathrm{in} \, (\lambda x.(\mathrm{let}\, a' = 0\, \mathrm{in}\, xa'))a \,\, \rightarrow\,\,\mathrm{let}\, a=1\, \mathrm{in}\, (\mathrm{let}\, a' = 0\, \mathrm{in}\, aa' ) $$

и некорректна, например, такая

$$\mathrm{let}\, a=1\, \mathrm{in}\, (\lambda x.(\mathrm{let}\, a = 0 \,\mathrm{in}\, xa))a \,\, \rightarrow\,\, \mathrm{let}\, a=1\, \mathrm{in} \, (\mathrm{let}\, a = 0\, \mathrm{in}\, aa ) .$$

Последняя, как видится, отвечает динамическому связыванию. Получается, что в λ-исчислении запрещен правилами редукции динамический аналог связывания? А как его тогда исследовать средствами λ-исчисления?

[Mysterious Light]

Многие авторы не желают возится с $\alpha$-проблемой в силу интуитивной неочевидности необходимости постоянного контроля имён. Их можно понять с позиции кодера: есть ли желание, определяя новую переменную, думать о том, что где-то там, вне кода конкретой функции, которую пишите лично Вы, есть другая переменная с тем же именем?

К слову, многие не называют это правило $\alpha$-редукцией, предпочитая называть это конверсией (т.е. преобразованием). Так, Барендрегт в книге «Лямбда-исчисление, синтаксис и семантика» вообще предлагает не анализировать $\alpha$-правило, считая его синтаксической условностью. Иными словами, мы на синтаксическом уровне не способны различать $\alpha$-эквивалентные термы — таково его предложение. Можно согласиться и оставить лишний формализм. А можно и ввести способы описать его: так, имеется формализм де-Брейна, который не предполагает использования переменных привычным для нас образом, но устраняет необходимость в $\alpha$-конверсии. Конечно, это исключает или серьёзно усложняет процесс динамического связывания. Но тут хотелось бы задать вопрос: как часто Вы применяете динамическое связывание на практике? Насколько этот вид связывания существеннен для Вас?

Одним из способов ввести динамическое связывание может быть метод контекстов. Контекст имеет определение, сходное с термом, за одним исключением: в качестве «атомарного значение» может выступать не только буквы алфавита aka переменные, но и буква/буквы специального вида. Они называются «дырками». При этом $\alpha$-конверсия не позволяет менять дырки и переменные. Также вводится процесс замещения дырки, когда один терм подставляется всюду вместо дырки так, что переменные терма связываются с некоторыми абстракторами контекста. Прочитайте упомянутую книгу Х. Барендрегта, в которой подробно описываются особенности контекстов с одной дыркой, то есть в которой дырка встречает ровно один раз.

[_hum_]

Mysterious Light в сообщении #670944 писал(а):

Конечно, это исключает или серьёзно усложняет процесс динамического связывания.

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

Цитата:

Но тут хотелось бы задать вопрос: как часто Вы применяете динамическое связывание на практике? Насколько этот вид связывания существеннен для Вас?

Не часто. Но вот возникла потребность, и хочу с этим разобраться (в чем суть динамического связывания, в чем его вред/польза, совместимо ли оно со статическим и проч. Это легче всего было бы понять на примере лямбда исчисления.)

Mysterious Light в сообщении #670944 писал(а):

Одним из способов ввести динамическое связывание может быть метод контекстов. Контекст имеет определение, сходное с термом, за одним исключением: в качестве «атомарного значение» может выступать не только буквы алфавита aka переменные, но и буква/буквы специального вида.

Я так понимаю, это уже расширение лямбда-исчисления? А с исходным, все-таки, как - можно промоделировать динамическое связывание или нет?

Mysterious Light в сообщении #670944 писал(а):

Прочитайте упомянутую книгу Х. Барендрегта, в которой подробно описываются особенности контекстов с одной дыркой, то есть в которой дырка встречает ровно один раз.

Спасибо. При случае гляну.

[Mysterious Light]

_hum_ в сообщении #671097 писал(а):

Меня именно этот вопрос волнует - можно ли средствами классического лямбда-исчислении промоделировать языки программирования с динамическим связыванием и ленивой стратегией вычисления.

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

_hum_ в сообщении #671097 писал(а):

Не часто. Но вот возникла потребность, и хочу с этим разобраться (в чем суть динамического связывания, в чем его вред/польза, совместимо ли оно со статическим и проч. Это легче всего было бы понять на примере лямбда исчисления.)

Значит, приходилось? Вот один мой знакомый спросил, о чём вообще речь идёт в этой теме, и мне было сложно ему объяснить на примере зачем вообще нужно динамическое связывание. Оно лишь тем отличается от статического, что допускает связывание переменных во время редукции ($\beta$-редукции в первую очередь). Сразу возникает проблема с $\alpha$-конверсией. И сходу вопрос: пусть Вы хотите редуцировать $(\lambda xy.C[x,y])D[y]$ до $\lambda y.C[D[y],y]$ так, что $y$ свяжется абстрактором, где $C[x,y]$ и $D[y]$ — обычные (или необычные, всё-таки о гипотетической ситуацией говорим) $\lambda$-термы с явным вхождением $x$ и $y$, то почему бы Вам не записать это выражение в виде $(\lambda xy.C[xy,y])(\lambda y.D[y])$? Всё-таки терм мы формируем на основании наших потребностей, мыслей, и вопрос лишь в том, будет ли первая форма более понятна человеку, чем вторая.

_hum_ в сообщении #671097 писал(а):

Я так понимаю, это уже расширение лямбда-исчисления? А с исходным, все-таки, как - можно промоделировать динамическое связывание или нет?

Я долго думал и пришел к выводу, что известные мне системы не позволяют делать динамическое связывание.
Также мне кажется, что основная причина состоит в том, что строимые теории базируются на $\alpha$-инвариантности, что не допускается при динамическом связывании.
Как мне кажется (в очередной раз подчёркиваю в совершенной неуверенности высказываемых утверждений), для того, чтобы ввести динамическое связывание, нужно пересмотреть основу да так, чтоб не было $\alpha$-конверсии. Например, ввести упомянутое понятие контекста.
Другой путь заключается в том, чтобы не фиксировать $\alpha$ как конверсию, но возвести в статус редукции, т.е. $\lambda$-собственное бинарное отношение. Тогда можно саму $\alpha$-редукцию модифицировать или вовсе отменить. Полагаю, в такой модификации также можно достичь формализма динамического связывания.

[_hum_]

Mysterious Light в сообщении #671366 писал(а):

пусть Вы хотите редуцировать $(\lambda xy.C[x,y])D[y]$ до $\lambda y.C[D[y],y]$ так, что $y$ свяжется абстрактором, где $C[x,y]$ и $D[y]$ — обычные (или необычные, всё-таки о гипотетической ситуацией говорим) $\lambda$-термы с явным вхождением $x$ и $y$, то почему бы Вам не записать это выражение в виде $(\lambda xy.C[xy,y])(\lambda y.D[y])$? [...]вопрос лишь в том, будет ли первая форма более понятна человеку, чем вторая.

Да, думаю, Вы правы. Динамическое связывание, судя по всему, является механизмом, главным образом служащим для того, чтобы уйти от передачи данных через механизм "данные как аргументы функции". У меня оно возникло именно по этой причине (прикидывал, как можно в разрабатываемом языке минимальными средствами организовать вычисление одного и того же (содержащего очень много переменных) выражения в нескольких разных контекстах, не прибегая к громоздкой передаче уймы аргументов функции). Первые пару ссылок google по запросу "What are the advantages of dynamic scoping?" вроде бы тоже подтверждают это.

Mysterious Light в сообщении #671366 писал(а):

можно саму $\alpha$-редукцию модифицировать или вовсе отменить. Полагаю, в такой модификации также можно достичь формализма динамического связывания.

Могу сказать только +1. У меня аналогичные мысли. :) Единственное, тогда наверное конфлюэнтность полетит в тар-тарары, и придется по-отдельности рассматривать случаи с разными порядками редукции.

Спасибо, что понимаете в чем мои затруднения и помогаете разбираться!