Перепост с dxdy.ru (интересно мнение здешней публики).

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

1) значение < — > всякий λ-терм в нормальной форме (относительно βη-редукции), например, λf.λx.x := 0, λf.λx.f x := 1
2) выражение <-> всякий λ-терм
3) вычисление выражения <-> алгоритмически заданный процесс преобразования исходного выражения к значению;
4) аппликативная/нормальная стратегия вычисления <-> вычисления с аппликативным/нормальным порядком редукции;
5) программа/исходные данные программы <-> λ-терм/значение к которому он будет применяться
6) декларирование (связывание идентификатора x с некоторым объектом) <-> констатация по терму вида (λx.P)V того факта, что в терме P при β-редукции вхождения связанной переменной x будут замещаться связанным с ней термом (объектом) V.

Пример. Конструкцию (λa.(λx.ax))1 можно, например, воспринимать как аналог let a = 1 in λx.ax.

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

Пример. С точки зрения λ-исчисления корректна такая последовательность редукций

(λa.(λx.(λa.xa)0)a)1 -> (λa.(λx.(λa'.xa')0)a)1 -> (λa.(λa'.aa')0)1

то есть,

let a=1 in (λx.(let a = 0 in xa))a -> let a=1 in (λx.(let a' = 0 in xa'))a -> let a=1 in (let a' = 0 in aa' )

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

let a=1 in (λx.(let a = 0 in xa))a -> let a=1 in (let a = 0 in aa ) .

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

Здравствуйте, _hum_, Вы писали:
__>9) статическое (лексическое) связывание <-> требование "неприкосновенности деклараций" при β-редукции, что выражается в требовании особым обрзом осуществлять подстановку, разводя путем α-редукции пересекающиеся имена переменных, если это может привести к изменению их декларативной связи с объектом.

__>Пример. С точки зрения λ-исчисления корректна такая последовательность редукций

__> (λa.(λx.(λa.xa)0)a)1 -> (λa.(λx.(λa'.xa')0)a)1 -> (λa.(λa'.aa')0)1

__>то есть,

__> let a=1 in (λx.(let a = 0 in xa))a -> let a=1 in (λx.(let a' = 0 in xa'))a -> let a=1 in (let a' = 0 in aa' )

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

__>let a=1 in (λx.(let a = 0 in xa))a -> let a=1 in (let a = 0 in aa ) .

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

Можете подробнее пояснить, в чём здесь аналогия со статическим/динамическим связыванием? Мне это совершенно не очевидно. В любом случае она не может быть слишком глубокой, поскольку лямбда-исчисление может быть легко переформулировано из терминов именованных переменных в термины индексов де Брёйна, где такого конфликта имён просто нет.

Здравствуйте, deniok, Вы писали:

D>Здравствуйте, _hum_, Вы писали:
__>>9) статическое (лексическое) связывание <-> требование "неприкосновенности деклараций" при β-редукции, что выражается в требовании особым обрзом осуществлять подстановку, разводя путем α-редукции пересекающиеся имена переменных, если это может привести к изменению их декларативной связи с объектом.

__>>Пример. С точки зрения λ-исчисления корректна такая последовательность редукций

__>> (λa.(λx.(λa.xa)0)a)1 -> (λa.(λx.(λa'.xa')0)a)1 -> (λa.(λa'.aa')0)1

__>>то есть,

__>> let a=1 in (λx.(let a = 0 in xa))a -> let a=1 in (λx.(let a' = 0 in xa'))a -> let a=1 in (let a' = 0 in aa' )

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

__>>let a=1 in (λx.(let a = 0 in xa))a -> let a=1 in (let a = 0 in aa ) .

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

D>Можете подробнее пояснить, в чём здесь аналогия со статическим/динамическим связыванием?
Вот есть у вас некоторый псевдоязык, поддерживающий анонимные функции (в формате λ<param>.(<body>) ) и осуществляющий "ленивые" вычисления. Тогда какое значение выдаст программа

let a = 2 in (λx.(let a = 1 in x * a))(a + 1)

при статическом связывании переменных, а какое при динамическом? При статическом, когда отложенное из ленивости вычислений выражение аргумента a+1 передается внутрь анонимной функции, происходит автоматическое переименование всех одноименных внутренних локальных переменных этой функции (α-конверсия), а именно,

(λx.(let a = 1 in x * a))(a + 1) -> let a' = 1 in (a + 1) * a' -> (2+1)*1 -> ...

При динамическом ничего подобного не делается — происходит прямая подстановка:

(λx.(let a = 1 in x * a))(a + 1) -> let a = 1 in (a + 1) * a -> (1+1)*1 -> ...

Так вот второй вариант в λ-исчислении недопустим (недопустима подстановка, которая привела бы к превращению свободной λ-переменной в связанную — требование сapture-avoiding substitutions).

Здравствуйте, _hum_, Вы писали:

D>>Можете подробнее пояснить, в чём здесь аналогия со статическим/динамическим связыванием?
__>Вот есть у вас некоторый псевдоязык, поддерживающий анонимные функции (в формате λ<param>.(<body>) ) и осуществляющий "ленивые" вычисления. Тогда какое значение выдаст программа

__>

__>let a = 2 in (λx.(let a = 1 in x * a))(a + 1)
__>

__>при статическом связывании переменных, а какое при динамическом?

Не-не-не, так не пойдёт. Вы от языка как-то перескочили к вычислителю, причём для определенной модели вычислений (Фон Неймановской), где есть переменные как хранилища в памяти и связывание имён с адресами этих хранилищ. Стандартный "простой" вычислитель для лямбда-исчисления гораздо глупее: он берёт лямбда-терм (дерево) ищет редекс (левый внешний для нормальной стратегии, правый внутренний для аппликативной) и делает бета-редукцию в соответствии с механизмом подстановки, подменяя замещаемые листья-переменные замещающим термом-деревцем. Никаких переменных, под которые выделены ячейки памяти, в лямбде нет. Говоря в ваших терминах имена переменных (связанных в смысле лямбда-исчисления) всегда связываются динамически, переставая существовать в момент связывания

Здравствуйте, deniok, Вы писали:

D>Не-не-не, так не пойдёт. Вы от языка как-то перескочили к вычислителю, причём для определенной модели вычислений (Фон Неймановской), где есть переменные как хранилища в памяти и связывание имён с адресами этих хранилищ.

Откуда вы это взяли? В примере у меня нигде нет ячеек — всюду чистые переменные. Возможно, вы как-то по-иному понимаете статическое и динамическое связывание. Я веду речь о Lexical scoping/Dynamic scoping из wiki/Scope(computer_science)

Здравствуйте, _hum_, Вы писали:

__>Здравствуйте, deniok, Вы писали:

D>>Не-не-не, так не пойдёт. Вы от языка как-то перескочили к вычислителю, причём для определенной модели вычислений (Фон Неймановской), где есть переменные как хранилища в памяти и связывание имён с адресами этих хранилищ.

__>Откуда вы это взяли? В примере у меня нигде нет ячеек — всюду чистые переменные. Возможно, вы как-то по-иному понимаете статическое и динамическое связывание. Я веду речь о Lexical scoping/Dynamic scoping из wiki/Scope(computer_science)

Ну понятно, трудности перевода
Я когда говорят про связывание переменной, подразумеваю variable binding, а scoping перевожу как область видимости.

Здравствуйте, deniok, Вы писали:

D>Здравствуйте, _hum_, Вы писали:

__>>Здравствуйте, deniok, Вы писали:

D>>>Не-не-не, так не пойдёт. Вы от языка как-то перескочили к вычислителю, причём для определенной модели вычислений (Фон Неймановской), где есть переменные как хранилища в памяти и связывание имён с адресами этих хранилищ.

__>>Откуда вы это взяли? В примере у меня нигде нет ячеек — всюду чистые переменные. Возможно, вы как-то по-иному понимаете статическое и динамическое связывание. Я веду речь о Lexical scoping/Dynamic scoping из wiki/Scope(computer_science)

D>Ну понятно, трудности перевода
D>Я когда говорят про связывание переменной, подразумеваю variable binding, а scoping перевожу как область видимости.

Так scope — это область действия связывания (binding-а). Потому в данном случае принципиальной разницы нет — при lexical scoping — связывание по статическому принципу, при dynamic scoping — по динамическому. Могу для вас перефразировать свой вопрос так: получается, что в λ-исчислении запрещен правилами редукции вариант вычислений с динамической областью действия связывания?

Здравствуйте, _hum_, Вы писали:

D>>Ну понятно, трудности перевода
D>>Я когда говорят про связывание переменной, подразумеваю variable binding, а scoping перевожу как область видимости.

__>Так scope — это область действия связывания (binding-а). Потому в данном случае принципиальной разницы нет — при lexical scoping — связывание по статическому принципу, при dynamic scoping — по динамическому. Могу для вас перефразировать свой вопрос так: получается, что в λ-исчислении запрещен правилами редукции вариант вычислений с динамической областью действия связывания?

Вы здесь понимаете под вычислением что-то отличное от выполнения редукций над термом? Если да, то это уже не лямбда-исчисление, а какая-то его реализация на каком-то стороннем вычислителе, и вы говорите о свойствах этого вычислителя. Если нет, то я не понимаю, что такое "динамическая область действия связывания". Глобальный стек связываний идентификаторов не нужен, потому что каждый идентификатор, связанный лямбдой, интересен вычислителю ровно один раз — когда эта лямбда редуцируется.

Здравствуйте, deniok, Вы писали:

D>Вы здесь понимаете под вычислением что-то отличное от выполнения редукций над термом?

см. мой первый пост

3) вычисление выражения <-> алгоритмически заданный процесс преобразования исходного выражения к значению;

Лямбда-исчисление само по себе не является полноценно заданной моделью вычислений (системой, на которой можно задавать алгоритмы). О последней можно вести речь только после того, как будет дополнительно указан алгоритм редукции λ-выражения. Например, алгоритм, который состоит в последовательном применении бета-редукцию к самому правому внутреннему редексу, приводит к модели вычислений, характерной для "жадных" вычислений со статическим связыванием. Так вот я говорю, что ни при каком заданном алгоритме редукции из лямбда-исчисления нельзя получить аналог модели вычислений с динамическим связыванием (с динамической областью действия связывания). [Это следует хотя бы из того, что модели с динамическим и статическим связыванием в общем случае дают разные результаты, тогда как λ-исчисление в силу свойства конфлюэнтности ни при каком алгоритме редукции не может давать разные результаты.]

Здравствуйте, _hum_, Вы писали:

__>Лямбда-исчисление само по себе не является полноценно заданной моделью вычислений (системой, на которой можно задавать алгоритмы). О последней можно вести речь только после того, как будет дополнительно указан алгоритм редукции λ-выражения. Например, алгоритм, который состоит в последовательном применении бета-редукцию к самому правому внутреннему редексу, приводит к модели вычислений, характерной для "жадных" вычислений со статическим связыванием. Так вот я говорю, что ни при каком заданном алгоритме редукции из лямбда-исчисления нельзя получить аналог модели вычислений с динамическим связыванием (с динамической областью действия связывания). [Это следует хотя бы из того, что модели с динамическим и статическим связыванием в общем случае дают разные результаты, тогда как λ-исчисление в силу свойства конфлюэнтности ни при каком алгоритме редукции не может давать разные результаты.]

Ok, зайдём с другой стороны. Берём ваш пример. Его можно записать либо целиком на лямбдах, либо целиком на let (ваша частичная запись, как мне кажется, вносит путаницу):

(λa. (λx. (λa. x * a) 1) (a + 1)) 2

let a = 2 in 
  (let x = (a + 1) in 
     (let a = 1 in x * a))

Вот держите естественную интерпретацию этого добра в энергичном императивном языке с динамическим скоупом, с тем же результатом 3, что и при любой правильной редукции

fun f()
{
  a = 2;
  return g();
}

fun g()
{
  x = a + 1;
  return h();
}

fun h()
{
  a = 1;
  return  x * a;
}

Здравствуйте, deniok.
Ладно, уточним — речь о динамическом связывании при "ленивых" (а не "энергичных") вычислениях. То есть, для варианта

let a = 2 in 
  (let x = (a + 1) in 
     (let a = 1 in x * a))

дающего результат 2, какой будет аналог в лямбда-исчислении?

Здравствуйте, _hum_, Вы писали:

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

На мой взгляд в классическом исчислении это невозможно.

Поискал в интернете, нашел работы, расширяющие классическое исчисление:
A Lambda-Calculus for Dynamic Binding
Dynamic Lambda Calculus

Здравствуйте, _hum_, Вы писали:

__>Здравствуйте, deniok.
__>Ладно, уточним — речь о динамическом связывании при "ленивых" (а не "энергичных") вычислениях. То есть, для варианта
__>

__>let a = 2 in 
__>  (let x = (a + 1) in 
__>     (let a = 1 in x * a))
__>

__>дающего результат 2, какой будет аналог в лямбда-исчислении?

Откуда тут вообще результат 2? Это просто плод ошибочной реализации подстановки. При ленивом вычислении сначала сократится внешний редекс — все свободные вхождения a заместятся двойкой, затем то же самое произойдёт с x и, наконец, с внутренним a

let a = 2 in 
  (let x = (a + 1) in 
     (let a = 1 in x * a))
->
let x = (2 + 1) in 
  (let a = 1 in x * a)
->
let a = 1 in (2 + 1) * a
->
(2 + 1) * 1

При энергичном на каждом шаге будет сокращаться правый внутренний редекс

let a = 2 in 
  (let x = (a + 1) in 
     (let a = 1 in x * a))
->
let a = 2 in 
  (let x = (a + 1) in 
     x * 1
->
let a = 2 in 
     (a + 1) * 1
->
(2 + 1) * 1

Ответом в любом случае будет тройка.

Здравствуйте, deniok.

А не так — при ленивом с динамическим связыванием:

Context = {}
let a = 2 in 
  (let x = (a + 1) in 
    (let a = 1 in x * a))
->
Context = {a->2}
let x = (a + 1) in 
  (let a = 1 in x * a)
->
Context = {a->2, x -> a+1}
  let a = 1 in x*a
->
Context = {a->1, x -> a+1}
x*a 
->
(1 + 1)*1
->
2

при ленивом со статическим связыванием:

Context = {}
let a = 2 in 
  (let x = (a + 1) in 
    (let a = 1 in x * a))
->
Context = {a->2}
let x = (a + 1) in 
  (let a = 1 in x * a)
->
Context = {a->2, x -> a+1}
  let a = 1 in x*a
->
Context = {a->2, a'->1, x -> a+1}
x*a' 
->
(2 + 1)*1
-> 
3

?

И если нет, то к какому классу вычислений относится первое приведенное мною?

Здравствуйте, _hum_, Вы писали:

__>Здравствуйте, deniok.

__>А не так — при ленивом с динамическим связыванием:

skiped

__>при ленивом со статическим связыванием:

skiped

__>И если нет, то к какому классу вычислений относится первое приведенное мною?


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

Здравствуйте, deniok, Вы писали:

D>Здравствуйте, _hum_, Вы писали:

__>>Здравствуйте, deniok.

__>>А не так — при ленивом с динамическим связыванием:

D>skiped

__>>при ленивом со статическим связыванием:

D>skiped

__>>И если нет, то к какому классу вычислений относится первое приведенное мною?


D>Я-то откуда знаю, это ваши вычислители, относите их к какому угодно классу.

Что значит, относите к какому угодно? Есть же общепринятые понятия вычислений со статическим/динамическим связыванием. В моем понимании ленивые вычисление с динамическим связыванием — это вычисления, которые осуществляются так, как я написал, а не так как вы (у меня, в отличие от вашего, не производится сразу подстановка значения в выражение).
Вот, может, это поможет понять о чем речь: в упоминавшейся вами книге John C. Mitchell, Foundations for Programming Languages в упражнении 2.2.13 описывается схожая ситуация.:

let x = 1 in 
   let f(y) = x + y in
     let x = 4 in
         f(5)

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

Здравствуйте, _hum_, Вы писали:

D>>Я-то откуда знаю, это ваши вычислители, относите их к какому угодно классу.

__>Что значит, относите к какому угодно? Есть же общепринятые понятия вычислений со статическим/динамическим связыванием. В моем понимании ленивые вычисление с динамическим связыванием — это вычисления, которые осуществляются так, как я написал, а не так как вы (у меня, в отличие от вашего, не производится сразу подстановка значения в выражение).


Ещё раз: как это делается в чистом лямбда-исчислении при выбранной стратегии редукций — я описал два поста назад. Вы мне приводите какие-то описания контекстов и их изменений. Это уже некоторая реализация, которую мы сами наделяем определенными свойствами.

__>Вот, может, это поможет понять о чем речь: в упоминавшейся вами книге John C. Mitchell, Foundations for Programming Languages в упражнении 2.2.13 описывается схожая ситуация.:

__>

__>let x = 1 in 
__>   let f(y) = x + y in
__>     let x = 4 in
__>         f(5) 
__>

__>в которой в зависимости от подхода к связыванию получаются два разных результата.

Да, я уже понял идею по вашим постам. Мне кажется, что необходимое для динамического скоупинга отслеживание control flow (когда он входит и когда покидает данную область видимости) для лямбда-терма определяется плохо. У нас же здесь нет инструкций, которые мы бы последовательно выполняли, как это было бы в императивных языках.

Здравствуйте, deniok, Вы писали:

D>Здравствуйте, _hum_, Вы писали:

D>Ещё раз: как это делается в чистом лямбда-исчислении при выбранной стратегии редукций — я описал два поста назад. Вы мне приводите какие-то описания контекстов и их изменений. Это уже некоторая реализация, которую мы сами наделяем определенными свойствами.

Только не "делается", а "делалось бы", если бы программа

П:
let a = 2 in 
  (let x = (a + 1) in 
    (let a = 1 in x * a))

была всего лишь вариантом записи лямбда-выражения

λ-П:
(λa. (λx. (λa. x * a) 1) (a + 1)) 2

На самом же деле стоит другая задача. Допустим, что представленная программа П является программой, написанной на каком-то языке с динамическим связыванием и ленивыми вычислениями. Вопрос: какая ей тогда соответствует программа на языке лямбда-исчисления? (Для случая статического связывания все просто — искомая λ-программа — это приведенная программа λ-П, а вот как быть с динамическим связыванием...).


__>>Вот, может, это поможет понять о чем речь: в упоминавшейся вами книге John C. Mitchell, Foundations for Programming Languages в упражнении 2.2.13 описывается схожая ситуация.:

__>>

__>>let x = 1 in 
__>>   let f(y) = x + y in
__>>     let x = 4 in
__>>         f(5) 
__>>

__>>в которой в зависимости от подхода к связыванию получаются два разных результата.

D>Да, я уже понял идею по вашим постам. Мне кажется, что необходимое для динамического скоупинга отслеживание control flow (когда он входит и когда покидает данную область видимости) для лямбда-терма определяется плохо. У нас же здесь нет инструкций, которые мы бы последовательно выполняли, как это было бы в императивных языках.

Так, что, получается, все-таки нельзя на лямбдах промоделировать динамическое связывание? А что тогда означает в том же упражнении 2.2.13 пункт

(c) Under dynamical scope, the binding for x in the body of f changes when f is called in the scope of the inner binding of x. Therefore, under dynamic scope, the value of this expression will be 4 + 5 = 9. Show how you can reduce expression to 9 by not renaming bound variables when you perform substitution.

Судя по написанному (подчеркнутому), все-таки как-то можно выполнять редукцию с тем, чтобы получить результат как при динамическом связывании, или я что-то не так понял?

Здравствуйте, _hum_, Вы писали:

D>>Да, я уже понял идею по вашим постам. Мне кажется, что необходимое для динамического скоупинга отслеживание control flow (когда он входит и когда покидает данную область видимости) для лямбда-терма определяется плохо. У нас же здесь нет инструкций, которые мы бы последовательно выполняли, как это было бы в императивных языках.

__>Так, что, получается, все-таки нельзя на лямбдах промоделировать динамическое связывание? А что тогда означает в том же упражнении 2.2.13 пункт
__>

__>(c) Under dynamical scope, the binding for x in the body of f changes when f is called in the scope of the inner binding of x. Therefore, under dynamic scope, the value of this expression will be 4 + 5 = 9. Show how you can reduce expression to 9 by not renaming bound variables when you perform substitution.

__>Судя по написанному (подчеркнутому), все-таки как-то можно выполнять редукцию с тем, чтобы получить результат как при динамическом связывании, или я что-то не так понял?

Я ничего не могу сказать по этому поводу, потому что я не знаю точной операционной семантики этой программы under dynamic scope. Где границы скоупов, каков стек вызовов, в какой момент и до какого состояния (nf, hnf, whnf) редуцируются термы и внешние функции вроде (+). Я вот, например, могу заметить, что любой нормальный функциональный язык (и ленивый, типа Haskell, и энергичный, типа ML) начнёт редукцию (λa. (λx. (λa. x * a) 1) (a + 1)) 2 с сокращения внешнего редекса. В тело лямбды никто никогда не лезет без нужды. Другое дело, что ML, если бы вместо 2 стоял бы редекс, сократил сначала его, а Haskell нет. После подстановки 2 получим (λx. (λa. x * a) 1) (2 + 1) (в реализации ленивого языка может быть не подстановка 2, а помещение на её место указателя на ячейку в которой лежит 2). Следующим шагом ML сложит 2 и 1, получив 3, а Хаскелл подставит вместо x указатель на ячейку, где лежит сумма отложенной 2 и 1. И т.д.

Та аналогия, которую вы пытаетесь провести вслед за Митчеллом, что вычисления под dynamic scoping похожи на порченную отсутствием альфа-конверсии бета-редукцию, она да, имеет место. Только я ничего фундаментального в ней не вижу, да и Митчелл тоже не особо это наблюдение использует в дальнейшем.

Здравствуйте, deniok, Вы писали:

D>Та аналогия, которую вы пытаетесь провести вслед за Митчеллом, что вычисления под dynamic scoping похожи на порченную отсутствием альфа-конверсии бета-редукцию, она да, имеет место. Только я ничего фундаментального в ней не вижу, да и Митчелл тоже не особо это наблюдение использует в дальнейшем.

Фундаментальность (по крайней мере для меня) в том, что из-за наличия требования альфа-конверсии лямбда-исчисление принципиально не допускает моделирования вычислений с динамическим связыванием. Получается, что лямбда-исчисление "затачивалось" под моделирование языков только со статическим связыванием. А если так, то на чем же тогда, интересно, строится теория языков с динамическим связыванием?