Читаю книжку Дж. Харрисона "Введение в функциональное программирование", возникло несколько вопросов.
Во-первых, что из себя представляет комбинация (один из четырех видов лямбда-терма)? Правильно ли я понимаю, что запись u v подразумевает неявное присутствие бинарной операции, соответствующей применению u к v.
Если это так, то неясно что будет, когда u не является лямбдой (абстракцией по терминологии Харрисона), то есть как он в таком случае "применяется"?
Далее, что тогда означает запись u v w ? Если действительно имеется в виду бинарная операция, то для неё необходимо задать ассоциативность, иначе без скобок запись лишена смысла. Ассоциативность левая или правая?
Во-вторых, непонятно как получена такая лямбда-редукция?
(\x.x x x)(\x.x x x) -> (\x.x x x)(\x.x x x)(\x.x x x)
Здравствуйте, SergASh, Вы писали:
SAS>Во-первых, что из себя представляет комбинация (один из четырех видов лямбда-терма)? Правильно ли я понимаю, что запись u v подразумевает неявное присутствие бинарной операции, соответствующей применению u к v.
Если я правильно понял вопрос (что не факт), то в лямбда-исчислении — всё есть лямбды, потому u v означает применение u к v.
SAS>Далее, что тогда означает запись u v w ? Если действительно имеется в виду бинарная операция, то для неё необходимо задать ассоциативность, иначе без скобок запись лишена смысла. Ассоциативность левая или правая?
Соответственно ((u v) w)
SAS>Во-вторых, непонятно как получена такая лямбда-редукция? SAS>(\x.x x x)(\x.x x x) -> (\x.x x x)(\x.x x x)(\x.x x x)
(\x.x x x) z -> z z z
Подставь теперь z = (\x.x x x), получишь
(\x.x x x)(\x.x x x)(\x.x x x)
Здравствуйте, VoidEx, Вы писали:
VE>Если я правильно понял вопрос (что не факт), то в лямбда-исчислении — всё есть лямбды, потому u v означает применение u к v.
Позволю себе процитировать (сокращённо)
Основой \-исчисления служит формальное понятие \-термов, которые строятся из переменных и некоторого фиксированного множества констант при помощи операцийприменения функций и \-абстракции. Это значит, что возможные \-термы разбиваются на 4 класса:
1. Переменные
2. Константы
3. Комбинации: применение функции s к аргументу t, где s и t представляют собой произвольные термы.
4. Абстракция произвольного \-терма s по переменной x; имеет вид \x.s
Вопрос в том, что означает u v, когда u относится к первому или второму классу.
SAS>Основой \-исчисления служит формальное понятие \-термов, которые строятся из переменных и некоторого фиксированного множества констант при помощи операцийприменения функций и \-абстракции. Это значит, что возможные \-термы разбиваются на 4 класса:
SAS>1. Переменные
SAS>2. Константы
SAS>3. Комбинации: применение функции s к аргументу t, где s и t представляют собой произвольные термы.
SAS>4. Абстракция произвольного \-терма s по переменной x; имеет вид \x.s
SAS>Вопрос в том, что означает u v, когда u относится к первому или второму классу.
А что они могут означать, кроме переменных и констант?
u v — это применение переменной u к переменной v, когда дойдёт дело до вычисления переменные получат значения.
А для констант это либо осмысленное выражение в рамках семантики этих констант, либо бессмысленное:
Ну, очевидно, что базой является 4-е.
\(переменные).(терм)
Константа — это какая-то фиксированная, но тоже лямбда.
Переменная принимает какое-то значение после применения и, само собой, может быть или лямбдой, или константой (тоже лямбдой).
Поэтому в 3-ем случае (применение функции s к аргументу t) s в любом случае лямбда, принимающая как минимум один аргумент, так что ничего ей не мешает принять t.
Поэтому (u v) — это применение u к v.
В тех же нумералах Чёрча:
0 = (\f x.x)
1 = (\f x.f x)
2 = (\f x.f (f x))
...
Ничего не мешает написать (1 2), будет применение 1 к 2.
(\f x.f x) (\g y.g (g y)) ->
\x.(\g y.g (g y)) x ->
\x.(\y.x (x y)) ->
\x y.x (x y) -> // переименуем x->f, y->x
\f x.f (f x) ->
2
Т.о. получили, что (1 2) редуцируется до 2.
VE>Константа — это какая-то фиксированная, но тоже лямбда.
У меня под рукой Харрисона нет, но для чистой лямбды, о которой ты говоришь, констант вводить не нужно, достаточно переменных, аппликации (применения) и абстракции. Константы — это как раз шаг к практической реализации (цифры, символы, встроенные операции +,-,*).
Здравствуйте, deniok, Вы писали:
D>Здравствуйте, VoidEx, Вы писали:
VE>>Константа — это какая-то фиксированная, но тоже лямбда.
D>У меня под рукой Харрисона нет, но для чистой лямбды, о которой ты говоришь, констант вводить не нужно, достаточно переменных, аппликации (применения) и абстракции. Константы — это как раз шаг к практической реализации (цифры, символы, встроенные операции +,-,*).
Я, видимо, неправильно понял. Я подумал, что под константами подразумевается как раз заданное значение с именем. Грубо говоря, обозначение (как 1 = (\f x. f x)). Вводить их не нужно, да, они для удобства.
Здравствуйте, SergASh, Вы писали:
SAS>Во-первых, что из себя представляет комбинация (один из четырех видов лямбда-терма)? Правильно ли я понимаю, что запись u v подразумевает неявное присутствие бинарной операции, соответствующей применению u к v.
SAS>Если это так, то неясно что будет, когда u не является лямбдой (абстракцией по терминологии Харрисона), то есть как он в таком случае "применяется"?
SAS>Далее, что тогда означает запись u v w ? Если действительно имеется в виду бинарная операция, то для неё необходимо задать ассоциативность, иначе без скобок запись лишена смысла. Ассоциативность левая или правая?
Лямбда-исчисление — это в первую очередь математическая теория — вид логики. Поэтому нет такого понятия как применяется. Есть набор операций для определения корректных выражений и есть набор правил преобразования одних выражений в другие.
Если есть правило, что можно взять два выражения а и б и поставить их вместе, значит надо относится к этому как к данности, а не искать скрытые бинарные операции.
В этом свете второй вопрос становится бессмысленным: если u не имеет вид (\x ...) то мы не сможем применить ни одно из правил преобразования, кроме переименования может быть. При этом терм остается абсолютно корректным лямбда-термом.
Трактовка u v w зависит от того, каких соглашений придерживается автор. Это не имеет отношения к бинарности операции, поскольку лямбда выражения составляются однозначно, а скобки опускаются только для удобства.
