Перепост с 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) статическое (лексическое) связывание <-> требование "неприкосновенности деклараций" при β-редукции, что выражается в требовании особым обрзом осуществлять подстановку, разводя путем α-редукции пересекающиеся имена переменных, если это может привести к изменению их декларативной связи с объектом.
Пример. С точки зрения λ-исчисления корректна такая последовательность редукций
Здравствуйте, _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 ) .
__>Последняя, как видится, отвечает динамическому связыванию. Получается, что в λ-исчислении запрещен правилами редукции динамический аналог связывания?
Можете подробнее пояснить, в чём здесь аналогия со статическим/динамическим связыванием? Мне это совершенно не очевидно. В любом случае она не может быть слишком глубокой, поскольку лямбда-исчисление может быть легко переформулировано из терминов именованных переменных в термины индексов де Брёйна, где такого конфликта имён просто нет.
Re[2]: Базовые концепты computer science на примере λ-исчисления
Здравствуйте, 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).
Re[3]: Базовые концепты computer science на примере λ-исчисления
Здравствуйте, _hum_, Вы писали:
D>>Можете подробнее пояснить, в чём здесь аналогия со статическим/динамическим связыванием? __>Вот есть у вас некоторый псевдоязык, поддерживающий анонимные функции (в формате λ<param>.(<body>) ) и осуществляющий "ленивые" вычисления. Тогда какое значение выдаст программа
__>
__>let a = 2 in (λx.(let a = 1 in x * a))(a + 1)
__>
__>при статическом связывании переменных, а какое при динамическом?
Не-не-не, так не пойдёт. Вы от языка как-то перескочили к вычислителю, причём для определенной модели вычислений (Фон Неймановской), где есть переменные как хранилища в памяти и связывание имён с адресами этих хранилищ. Стандартный "простой" вычислитель для лямбда-исчисления гораздо глупее: он берёт лямбда-терм (дерево) ищет редекс (левый внешний для нормальной стратегии, правый внутренний для аппликативной) и делает бета-редукцию в соответствии с механизмом подстановки, подменяя замещаемые листья-переменные замещающим термом-деревцем. Никаких переменных, под которые выделены ячейки памяти, в лямбде нет. Говоря в ваших терминах имена переменных (связанных в смысле лямбда-исчисления) всегда связываются динамически, переставая существовать в момент связывания
Re[4]: Базовые концепты computer science на примере λ-исчисления
Здравствуйте, deniok, Вы писали:
D>Не-не-не, так не пойдёт. Вы от языка как-то перескочили к вычислителю, причём для определенной модели вычислений (Фон Неймановской), где есть переменные как хранилища в памяти и связывание имён с адресами этих хранилищ.
Откуда вы это взяли? В примере у меня нигде нет ячеек — всюду чистые переменные. Возможно, вы как-то по-иному понимаете статическое и динамическое связывание. Я веду речь о Lexical scoping/Dynamic scoping из wiki/Scope(computer_science)
Re[5]: Базовые концепты computer science на примере λ-исчисления
Здравствуйте, _hum_, Вы писали:
__>Здравствуйте, deniok, Вы писали:
D>>Не-не-не, так не пойдёт. Вы от языка как-то перескочили к вычислителю, причём для определенной модели вычислений (Фон Неймановской), где есть переменные как хранилища в памяти и связывание имён с адресами этих хранилищ.
__>Откуда вы это взяли? В примере у меня нигде нет ячеек — всюду чистые переменные. Возможно, вы как-то по-иному понимаете статическое и динамическое связывание. Я веду речь о Lexical scoping/Dynamic scoping из wiki/Scope(computer_science)
Ну понятно, трудности перевода
Я когда говорят про связывание переменной, подразумеваю variable binding, а scoping перевожу как область видимости.
Re[6]: Базовые концепты computer science на примере λ-исчисления
Здравствуйте, deniok, Вы писали:
D>Здравствуйте, _hum_, Вы писали:
__>>Здравствуйте, deniok, Вы писали:
D>>>Не-не-не, так не пойдёт. Вы от языка как-то перескочили к вычислителю, причём для определенной модели вычислений (Фон Неймановской), где есть переменные как хранилища в памяти и связывание имён с адресами этих хранилищ.
__>>Откуда вы это взяли? В примере у меня нигде нет ячеек — всюду чистые переменные. Возможно, вы как-то по-иному понимаете статическое и динамическое связывание. Я веду речь о Lexical scoping/Dynamic scoping из wiki/Scope(computer_science)
D>Ну понятно, трудности перевода D>Я когда говорят про связывание переменной, подразумеваю variable binding, а scoping перевожу как область видимости.
Так scope — это область действия связывания (binding-а). Потому в данном случае принципиальной разницы нет — при lexical scoping — связывание по статическому принципу, при dynamic scoping — по динамическому. Могу для вас перефразировать свой вопрос так: получается, что в λ-исчислении запрещен правилами редукции вариант вычислений с динамической областью действия связывания?
Re[7]: Базовые концепты computer science на примере λ-исчисления
Здравствуйте, _hum_, Вы писали:
D>>Ну понятно, трудности перевода D>>Я когда говорят про связывание переменной, подразумеваю variable binding, а scoping перевожу как область видимости.
__>Так scope — это область действия связывания (binding-а). Потому в данном случае принципиальной разницы нет — при lexical scoping — связывание по статическому принципу, при dynamic scoping — по динамическому. Могу для вас перефразировать свой вопрос так: получается, что в λ-исчислении запрещен правилами редукции вариант вычислений с динамической областью действия связывания?
Вы здесь понимаете под вычислением что-то отличное от выполнения редукций над термом? Если да, то это уже не лямбда-исчисление, а какая-то его реализация на каком-то стороннем вычислителе, и вы говорите о свойствах этого вычислителя. Если нет, то я не понимаю, что такое "динамическая область действия связывания". Глобальный стек связываний идентификаторов не нужен, потому что каждый идентификатор, связанный лямбдой, интересен вычислителю ровно один раз — когда эта лямбда редуцируется.
Re[8]: Базовые концепты computer science на примере λ-исчисления
Здравствуйте, deniok, Вы писали:
D>Вы здесь понимаете под вычислением что-то отличное от выполнения редукций над термом?
см. мой первый пост
3) вычисление выражения <-> алгоритмически заданный процесс преобразования исходного выражения к значению;
Лямбда-исчисление само по себе не является полноценно заданной моделью вычислений (системой, на которой можно задавать алгоритмы). О последней можно вести речь только после того, как будет дополнительно указан алгоритм редукции λ-выражения. Например, алгоритм, который состоит в последовательном применении бета-редукцию к самому правому внутреннему редексу, приводит к модели вычислений, характерной для "жадных" вычислений со статическим связыванием. Так вот я говорю, что ни при каком заданном алгоритме редукции из лямбда-исчисления нельзя получить аналог модели вычислений с динамическим связыванием (с динамической областью действия связывания). [Это следует хотя бы из того, что модели с динамическим и статическим связыванием в общем случае дают разные результаты, тогда как λ-исчисление в силу свойства конфлюэнтности ни при каком алгоритме редукции не может давать разные результаты.]
Re[9]: Базовые концепты computer science на примере λ-исчисления
Здравствуйте, _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;
}
Re[10]: Базовые концепты computer science на примере λ-исчисления
Здравствуйте, _hum_, Вы писали:
__>Последняя, как видится, отвечает динамическому связыванию. Получается, что в ?-исчислении запрещен правилами редукции динамический аналог связывания?
На мой взгляд в классическом исчислении это невозможно.
Здравствуйте, _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
Ответом в любом случае будет тройка.
Re[12]: Базовые концепты computer science на примере λ-исчисления
А не так — при ленивом с динамическим связыванием:
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
?
И если нет, то к какому классу вычислений относится первое приведенное мною?
Re[13]: Базовые концепты computer science на примере λ-исчисления
Здравствуйте, _hum_, Вы писали:
__>Здравствуйте, deniok.
__>А не так — при ленивом с динамическим связыванием:
skiped
__>при ленивом со статическим связыванием:
skiped
__>И если нет, то к какому классу вычислений относится первое приведенное мною?
Я-то откуда знаю, это ваши вычислители, относите их к какому угодно классу. Я делал бета-редукцию в точности по стандартным правилам и редекс выбирал каждый раз левый внешний. В чистом лямбда-исчислении имя связанной лямбда-абстракцией переменной при сокращении редекса пропадает. Если оно вообще было, потому что реализации, интересующиеся эффективностью, обычно используют индексы де Брейна.
Re[14]: Базовые концепты computer science на примере λ-исчисления
Здравствуйте, 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)
в которой в зависимости от подхода к связыванию получаются два разных результата.
Re[15]: Базовые концепты computer science на примере λ-исчисления
Здравствуйте, _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 (когда он входит и когда покидает данную область видимости) для лямбда-терма определяется плохо. У нас же здесь нет инструкций, которые мы бы последовательно выполняли, как это было бы в императивных языках.
Re[16]: Базовые концепты computer science на примере λ-исчисления
Здравствуйте, 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.
Судя по написанному (подчеркнутому), все-таки как-то можно выполнять редукцию с тем, чтобы получить результат как при динамическом связывании, или я что-то не так понял?
Re[17]: Базовые концепты computer science на примере λ-исчисления
Здравствуйте, _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 похожи на порченную отсутствием альфа-конверсии бета-редукцию, она да, имеет место. Только я ничего фундаментального в ней не вижу, да и Митчелл тоже не особо это наблюдение использует в дальнейшем.
Re[18]: Базовые концепты computer science на примере λ-исчисления
Здравствуйте, deniok, Вы писали:
D>Та аналогия, которую вы пытаетесь провести вслед за Митчеллом, что вычисления под dynamic scoping похожи на порченную отсутствием альфа-конверсии бета-редукцию, она да, имеет место. Только я ничего фундаментального в ней не вижу, да и Митчелл тоже не особо это наблюдение использует в дальнейшем.
Фундаментальность (по крайней мере для меня) в том, что из-за наличия требования альфа-конверсии лямбда-исчисление принципиально не допускает моделирования вычислений с динамическим связыванием. Получается, что лямбда-исчисление "затачивалось" под моделирование языков только со статическим связыванием. А если так, то на чем же тогда, интересно, строится теория языков с динамическим связыванием?