ВУЗ:
Составители:
66
Для того, чтобы проверить необходимое свойство, обозначим терм λx y. y(x x y) через a.
Тогда имеем
T f ≡ (λx y. y(x x y)) a f →
β
f (a a f) ≡ f (T f)
9.2.5 Функции с несколькими аргументами
В математических обозначениях применение n–местной функции f к аргументам
x
1
… x
n
записывается как f (x
1
, …, x
n
). Существует два способа представления n–кратной
аппликации в λ–исчислении:
1) как ( f x
1
… x
n
), или
2) как аппликация f к n–ке (x
1
, …, x
n
).
В первом случае f применяется к своим аргументам по–очереди. Русский матема-
тик Шейфинкель заметил, что не обязательно вводить функции более чем одной перемен-
ной [15]. Действительно, для функции, скажем от двух переменных, f(x,y) мы можем рас-
смотреть функцию g
x
с соотношением g
x
(y) = f(x,y), а затем f' с соотношением f'(x) = g
x
.
Отсюда (f'(x))(y) = f(x,y). Позднее Карри [16] переоткрыл это свойство и поэтому сейчас
сведение функций с несколькими переменными только к функциям одного переменного
носит название карринг. Функции and, or или add, определенные ранее, применяют кар-
ринг. Преимущество функций с каррингом заключается в том, что такие функции можно
применять частично с меньшим числом аргументом, чем требуется по определению этих
функций. Например, add <1> есть результат частичного применения функции add к <1> и
обозначает функцию n → n+1.
Хотя часто удобно представлять n–местные функции с помощью карринга, полезно
также иметь возможность представлять аргументы с помощью единственной n-ки. На-
пример, вместо представления сложения λ–термом add, так что выполняется условие
add <m> <n> = <m+n>
может быть более удобно представить λ–термом sum, для которого выполнено
sum (<m>, <n>) = <m+n>
Таким образом, n–местные функции можно определить как с каррингом, так и без каррин-
га.
Можно определить два комбинатора, применяя которые к функциям, можно менять
наличие карринга у последних.
curry ≡ λ f x y. f (x, y)
uncurry ≡ λ f p. f (fst p) (snd p)
Имеем для произвольного выражения E:
curry (uncurry E) = E
uncurry (curry E) = E
Проверим первое равенство:
curry (uncurry E)
≡ (λ f x y. f (x, y)) (uncurry E)
Страницы
- « первая
- ‹ предыдущая
- …
- 64
- 65
- 66
- 67
- 68
- …
- следующая ›
- последняя »
