Лямбда-исчисление — различия между версиями
м (rollbackEdits.php mass rollback) |
|||
(не показаны 64 промежуточные версии 13 участников) | |||
Строка 1: | Строка 1: | ||
− | '''Лямбда-исчисление'''(''lambda calculus'') {{---}} формальная система, придуманная в 1930-х годах | + | '''Лямбда-исчисление''' (''англ. lambda calculus'') {{---}} формальная система, придуманная в 1930-х годах |
Алонзо Чёрчем. Лямбда-функция является, по сути, анонимной функцией. | Алонзо Чёрчем. Лямбда-функция является, по сути, анонимной функцией. | ||
Эта концепция показала себя удобной и сейчас активно используется во многих | Эта концепция показала себя удобной и сейчас активно используется во многих | ||
Строка 5: | Строка 5: | ||
== Лямбда-исчисление== | == Лямбда-исчисление== | ||
− | |||
− | |||
− | |||
{{Определение | {{Определение | ||
|definition= | |definition= | ||
+ | '''Лямбда-выражением''' (англ. <tex>\lambda</tex>''-term'') называется выражение, удовлетворяющее следующей грамматике:<br> | ||
<tex> | <tex> | ||
− | \ | + | \Lambda \to V\\ |
− | \ | + | \Lambda \to \Lambda \ \Lambda\\ |
− | + | \Lambda \to \lambda V . \Lambda | |
− | |||
− | |||
− | |||
− | |||
</tex> | </tex> | ||
+ | где <tex>V</tex> {{---}} множество всех строк над фиксированным алфавитом <tex> \Sigma \setminus \{ "\lambda", "\ ",\ "."\} </tex>. | ||
}} | }} | ||
+ | Пробел во втором правиле является терминалом грамматики. Иногда его обозначают как @, чтобы он не сливался с другими символами в выражении. | ||
В первом случае функция является просто переменной. | В первом случае функция является просто переменной. | ||
Строка 27: | Строка 23: | ||
создание функции одного аргумента с заданными именем аргумента и телом функции. | создание функции одного аргумента с заданными именем аргумента и телом функции. | ||
− | Рассмотрим, например, | + | Рассмотрим, например, <tex>\lambda</tex>-терм <tex>\operatorname{id} = \lambda x\ .\ x</tex>. Эта функция принимает аргумент и |
возвращает его неизменённым. Например, | возвращает его неизменённым. Например, | ||
<tex>\operatorname{id}\ 2 \equiv 2</tex>. Аналогично, <tex>\operatorname{id}\ y \equiv y</tex>. | <tex>\operatorname{id}\ 2 \equiv 2</tex>. Аналогично, <tex>\operatorname{id}\ y \equiv y</tex>. | ||
− | + | Еще примеры: | |
− | + | :<tex> | |
− | + | x\\ | |
+ | (x\ z)\\ | ||
+ | (\lambda x.(x\ z))\\ | ||
+ | (\lambda z.(\lambda w.((\lambda y.((\lambda x.(x\ z))\ y))\ w)))\\ | ||
+ | </tex> | ||
+ | |||
+ | Иногда <tex>\lambda</tex> -термы пишут по другому. Для краткости подряд идущие лямбды заменяют на одну. Например: | ||
+ | :<tex>\lambda x\ .\ \lambda y\ .P\ \to\ \lambda xy.P</tex> | ||
===Приоритет операций=== | ===Приоритет операций=== | ||
− | * | + | * Аппликация: <tex>x\ y\ z\ w \equiv ((x\ y)\ z)\ w</tex> |
* Абстракция забирает себе всё, до чего дотянется: <tex>\lambda x\ .\ \lambda y\ .\ \lambda z\ .\ z\ y\ x \equiv \lambda x\ .\ (\lambda y\ .\ (\lambda z\ .\ ((z\ y)\ x)))</tex> | * Абстракция забирает себе всё, до чего дотянется: <tex>\lambda x\ .\ \lambda y\ .\ \lambda z\ .\ z\ y\ x \equiv \lambda x\ .\ (\lambda y\ .\ (\lambda z\ .\ ((z\ y)\ x)))</tex> | ||
* Скобки играют привычную роль группировки действий | * Скобки играют привычную роль группировки действий | ||
Строка 44: | Строка 47: | ||
дереве разбора были абстракции. Все остальные переменные называются свободными. | дереве разбора были абстракции. Все остальные переменные называются свободными. | ||
− | Например, в <tex>\lambda x\ .\ | + | Например, в <tex>\lambda x\ .\ y\ x</tex>, <tex>x</tex> и связана, а <tex>y</tex>{{---}} свободна. А в <tex>\lambda y\ .\ x\ (\lambda x\ .\ x)</tex> |
в своём первом вхождении переменная <tex>x</tex> свободна, а во втором {{---}} связана. | в своём первом вхождении переменная <tex>x</tex> свободна, а во втором {{---}} связана. | ||
+ | |||
+ | Связанные переменные {{---}} это аргументы функции. То есть для функции они являются локальными. | ||
Рассмотрим функции <tex>\lambda y\ .\ y</tex> и <tex>\lambda x\ .\ y</tex>. В первой из них при взгляде на <tex>y</tex> | Рассмотрим функции <tex>\lambda y\ .\ y</tex> и <tex>\lambda x\ .\ y</tex>. В первой из них при взгляде на <tex>y</tex> | ||
Строка 55: | Строка 60: | ||
по <tex>x</tex>. | по <tex>x</tex>. | ||
− | ===α- | + | ===α-эквивалентность=== |
{{Определение | {{Определение | ||
− | |definition=''<tex>\alpha</tex>- | + | |definition='''<tex>\alpha</tex>-эквивалентностью''' (англ. ''<tex>\alpha</tex> -equivalence'') {{---}} называется наименьшее соотношение эквивалентности на <tex>\Lambda</tex> такое что: |
:<tex>P=_\alpha P</tex> для любого <tex>P</tex> | :<tex>P=_\alpha P</tex> для любого <tex>P</tex> | ||
:<tex>\lambda x.P=_\alpha \lambda y.P[x:=y]</tex> если <tex>y \not\in FV(P)</tex> | :<tex>\lambda x.P=_\alpha \lambda y.P[x:=y]</tex> если <tex>y \not\in FV(P)</tex> | ||
Строка 76: | Строка 81: | ||
{{Определение | {{Определение | ||
|definition= | |definition= | ||
− | <tex>\beta</tex>-редукция это наименьшее соотношение на <tex>\Lambda</tex> такое что | + | '''<tex>\beta</tex>-редукция''' (англ. ''<tex>\beta</tex> -reduction'') {{---}} это наименьшее соотношение на <tex>\Lambda</tex> такое что |
:<tex>(\lambda x.P)Q\to _\beta P[x:=Q]</tex> | :<tex>(\lambda x.P)Q\to _\beta P[x:=Q]</tex> | ||
и замкнуто относительно следующих правил | и замкнуто относительно следующих правил | ||
Строка 90: | Строка 95: | ||
}} | }} | ||
− | ==Нотация Де | + | В <tex>\beta</tex>-редукции вполне возможна функция вида <tex>\lambda x. \lambda x.x</tex>. Во время подстановки вместо <tex>x</tex> внутренняя переменная не заменяется - действует принцип локальной переменной. Но принято считать, что таких ситуаций не возникает и все переменные называются разными именами. |
+ | |||
+ | ===Каррирование=== | ||
+ | |||
+ | {{Определение | ||
+ | |definition= | ||
+ | '''Каррирование''' (англ. ''carrying'') {{---}} преобразование функции от многих переменных в функцию, берущую свои аргументы по одному. Для функции <tex>h</tex> типа <tex>h\ :\ (A\ *\ B)\ \to\ C</tex> оператор каррирования <tex>\Lambda </tex> выполняет преобразование <tex>\Lambda (h)\ :\ A\to (B\to C)</tex>. Таким образом <tex>\Lambda (h)</tex> берет аргумент типа <tex>A</tex> и возвращает функцию типа <tex>B\ \to\ C</tex>. С интуитивной точки зрения, каррирование функции позволяет фиксировать ее некоторый аргумент, возвращая функцию от остальных аргументов. Таким образом, <tex>\Lambda</tex> представляет собой функцию типа <tex>\Lambda :\ (A\ *\ B\to C)\to (A\to (B\to C))</tex>. | ||
+ | }} | ||
+ | |||
+ | ==Нотация Де Брауна== | ||
Существует также альтернативное эквивалентное определение <tex>\lambda</tex>-исчисления. | Существует также альтернативное эквивалентное определение <tex>\lambda</tex>-исчисления. | ||
В оригинальном определении для обозначения переменных использовались имена, | В оригинальном определении для обозначения переменных использовались имена, | ||
Строка 101: | Строка 115: | ||
связана. В данной нотации получаются несколько более простые определения | связана. В данной нотации получаются несколько более простые определения | ||
свободных переменных и <tex>\beta</tex>-редукции. | свободных переменных и <tex>\beta</tex>-редукции. | ||
+ | |||
+ | Грамматику нотации можно задать как: | ||
+ | :<tex>e\ ::= n\ |\ \lambda .e\ |\ e\ e</tex> | ||
+ | |||
+ | Примеры выражений в этой нотации: | ||
+ | |||
+ | {| | ||
+ | ! Standart | ||
+ | ! de Bruijn | ||
+ | |- | ||
+ | | $\lambda x.x$ | ||
+ | | $\lambda .0$ | ||
+ | |- | ||
+ | | $\lambda z.z$ | ||
+ | | $\lambda .0$ | ||
+ | |- | ||
+ | | $\lambda x. \lambda y.x$ | ||
+ | | $\lambda . \lambda .1$ | ||
+ | |- | ||
+ | | $\lambda x. \lambda y. \lambda s. \lambda z.x\ s\ (y\ s\ z)$ | ||
+ | | $\lambda . \lambda . \lambda . \lambda .3\ 1(2\ 1\ 0)$ | ||
+ | |- | ||
+ | | $(\lambda x.x\ x)(\lambda x.x\ x)$ | ||
+ | | $(\lambda .0\ 0)(\lambda .0\ 0)$ | ||
+ | |- | ||
+ | | $(\lambda x. \lambda x.x)(\lambda y.y)$ | ||
+ | | $(\lambda .\lambda .0)(\lambda .0)$ | ||
+ | |} | ||
Переменная называется свободной, если ей соответствует число, которое больше | Переменная называется свободной, если ей соответствует число, которое больше | ||
Строка 117: | Строка 159: | ||
число. | число. | ||
− | + | :<tex>\bar 0 = \lambda s\ .\ \lambda z\ .\ z</tex> | |
− | + | :<tex>\bar 1 = \lambda s\ .\ \lambda z\ .\ s\ z</tex> | |
− | + | :<tex>\bar 2 = \lambda s\ .\ \lambda z\ .\ s\ (s\ z)</tex> | |
− | + | :<tex>\bar 3 = \lambda s\ .\ \lambda z\ .\ s\ (s\ (s\ z))</tex> | |
Каждое число будет функцией двух аргументов: какой-то функции и начального значения. | Каждое число будет функцией двух аргументов: какой-то функции и начального значения. | ||
Строка 129: | Строка 171: | ||
===+1=== | ===+1=== | ||
− | Функция, прибавляющая 1 к числу, должна принимать первым аргументом число. | + | Функция, прибавляющая <tex>1</tex> к числу, должна принимать первым аргументом число. |
Но число {{---}} функция двух аргументов. Значит, эта функция должна принимать три | Но число {{---}} функция двух аргументов. Значит, эта функция должна принимать три | ||
аргумента: "число" <tex>n</tex>, которое хочется увеличить, функция, которую надо будет | аргумента: "число" <tex>n</tex>, которое хочется увеличить, функция, которую надо будет | ||
Строка 147: | Строка 189: | ||
<tex>(\operatorname{plus}\ \bar 3\ \bar 3)\ (+1)\ 0 \equiv 6</tex> | <tex>(\operatorname{plus}\ \bar 3\ \bar 3)\ (+1)\ 0 \equiv 6</tex> | ||
+ | |||
+ | <tex>(\operatorname{plus}\ ((\operatorname{plus}\ 2\ 5)(+1)\ 0)\ 4)(+1)0 \equiv 11</tex> | ||
===Умножение=== | ===Умножение=== | ||
Строка 194: | Строка 238: | ||
<tex>\operatorname{isZero} = \lambda n\ .\ n\ (\lambda c\ .\ \operatorname{false})\ \operatorname{true}</tex> | <tex>\operatorname{isZero} = \lambda n\ .\ n\ (\lambda c\ .\ \operatorname{false})\ \operatorname{true}</tex> | ||
− | Функция выглядит несколько странно. <tex>\lambda c | + | Функция выглядит несколько странно. <tex>\lambda c \to \operatorname{false}</tex> - функция, которая независимо |
от того, что ей дали на вход, возвращает <tex>\operatorname{false}</tex>. Тогда, если в качестве <tex>n</tex> | от того, что ей дали на вход, возвращает <tex>\operatorname{false}</tex>. Тогда, если в качестве <tex>n</tex> | ||
будет дан ноль, то функция, по определению нуля, не выполнится ни разу, и будет | будет дан ноль, то функция, по определению нуля, не выполнится ни разу, и будет | ||
Строка 237: | Строка 281: | ||
===Комбинатор неподвижной точки=== | ===Комбинатор неподвижной точки=== | ||
− | Попробуем выразить в лямбда-исчислении какую-нибудь функцию, использующую рекурсию. | + | Попробуем выразить в лямбда-исчислении какую-нибудь функцию, использующую рекурсию. Например, факториал. |
<tex>\operatorname{fact} = \lambda x\ .\ \operatorname{if}\ (\operatorname{isZero}\ x)\ \bar 1\ (\operatorname{fact}\ (\operatorname{pred}\ x))</tex> | <tex>\operatorname{fact} = \lambda x\ .\ \operatorname{if}\ (\operatorname{isZero}\ x)\ \bar 1\ (\operatorname{fact}\ (\operatorname{pred}\ x))</tex> | ||
Строка 271: | Строка 315: | ||
Это даст функцию, которая посчитает факториал числа. Но делать она это будет мееедленно-меееедленно. Для того, чтобы посчитать <tex>5!</tex> потребовалось сделать 66066 <tex>\beta</tex>-редукций. | Это даст функцию, которая посчитает факториал числа. Но делать она это будет мееедленно-меееедленно. Для того, чтобы посчитать <tex>5!</tex> потребовалось сделать 66066 <tex>\beta</tex>-редукций. | ||
− | + | Наиболее известным комбинатором неподвижной точки является <tex>Y</tex>-комбинатор, введенный известным американским ученым Хаскеллом Карри как | |
+ | :<tex>Y\ = \ \lambda f.(\lambda x.f(x\ x))\ (\lambda x.f(x\ x))</tex> | ||
===Деление=== | ===Деление=== | ||
Строка 288: | Строка 333: | ||
===Проверка на простоту=== | ===Проверка на простоту=== | ||
− | <tex>\operatorname{isPrimeHelp}</tex> {{---}} принимает число, которое требуется проверить на простоту и то, на что его надо опытаться поделить, перебирая это от 2 до <tex>p-1</tex>. Если на что-нибудь разделилось, то число {{---}} составное, иначе {{---}} простое. | + | <tex>\operatorname{isPrimeHelp}</tex> {{---}} принимает число, которое требуется проверить на простоту и то, на что его надо опытаться поделить, перебирая это от <tex>2</tex> до <tex>p-1</tex>. Если на что-нибудь разделилось, то число {{---}} составное, иначе {{---}} простое. |
<tex>\operatorname{isPrimeHelp'} =</tex><tex>\lambda f\ .\ \lambda p\ .\ \lambda i\ .\ \operatorname{if}\ (\operatorname{le}\ p\ i)\ \operatorname{true}\ (\operatorname{if}\ (\operatorname{isZero}\ (\operatorname{mod}\ p\ i))\ \operatorname{false}\ (f\ p\ (\operatorname{succ}\ i)))</tex> | <tex>\operatorname{isPrimeHelp'} =</tex><tex>\lambda f\ .\ \lambda p\ .\ \lambda i\ .\ \operatorname{if}\ (\operatorname{le}\ p\ i)\ \operatorname{true}\ (\operatorname{if}\ (\operatorname{isZero}\ (\operatorname{mod}\ p\ i))\ \operatorname{false}\ (f\ p\ (\operatorname{succ}\ i)))</tex> | ||
Строка 348: | Строка 393: | ||
====fact==== | ====fact==== | ||
− | (\f.(\x.f (x x)) (\x.f (x x))) (\f.\x.(\p.\t.\e.p t e) ((\n.n (\c.\a.\b.b) (\a.\b.a)) (x)) (\s.\z.s z) ((\n.\m.\s.n (m s)) (x) (f ((\n.\s.\z.(\p.p (\a.\b.b)) (n (\p.(\a.\b.\t.t a b) (s ((\p.p (\a.\b.a)) (p))) ((\p.p (\a.\b.a)) (p))) ((\a.\b.\t.t a b) (z) z))) (x))))) | + | <tex>(\lambda f.(\lambda x.f (x x))</tex><tex> (\lambda x.f (x x)))</tex><tex> (\lambda f.\lambda x.(\lambda p.\lambda t.\lambda e.p t e)</tex><tex> ((\lambda n.n (\lambda c.\lambda a.\lambda b.b)</tex><tex> (\lambda a.\lambda b.a))</tex><tex> (x))</tex><tex> (\lambda s.\lambda z.s z)</tex><tex> ((\lambda n.\lambda m.\lambda s.n (m s))</tex><tex> (x)</tex><tex> (f ((\lambda n.\lambda s.\lambda z.(\lambda p.p (\lambda a.\lambda b.b))</tex><tex> (n (\lambda p.(\lambda a.\lambda b.\lambda t.t a b)</tex><tex> (s ((\lambda p.p (\lambda a.\lambda b.a))</tex><tex> (p)))</tex><tex> ((\lambda p.p (\lambda a.\lambda b.a))</tex><tex> (p)))</tex><tex>((\lambda a.\lambda b.\lambda t.t a b)</tex><tex>(z)</tex><tex> z))) (x)))))</tex> |
− | |||
====head==== | ====head==== | ||
− | \list.(\f.(\x.f (x x)) (\x.f (x x))) (\f.\n.\m.(\p.\t.\e.p t e) ((\n.n (\c.\a.\b.b) (\a.\b.a)) ((\f.(\x.f (x x)) (\x.f (x x))) (\mod.\n.\m.(\p.\t.\e.p t e) ((\n.\m.(\n.\m.(\n.n (\c.\a.\b.b) (\a.\b.a)) ((\n.\m.m (\n.\s.\z.(\p.p (\a.\b.b)) (n (\p.(\a.\b.\t.t a b) (s ((\p.p (\a.\b.a)) (p))) ((\p.p (\a.\b.a)) (p))) ((\a.\b.\t.t a b) (z) z))) n) (n) m)) (n) ((\n.\s.\z.(\p.p (\a.\b.b)) (n (\p.(\a.\b.\t.t a b) (s ((\p.p (\a.\b.a)) (p))) ((\p.p (\a.\b.a)) (p))) ((\a.\b.\t.t a b) (z) z))) (m))) (n) m) n (mod ((\n.\m.m (\n.\s.\z.(\p.p (\a.\b.b)) (n (\p.(\a.\b.\t.t a b) (s ((\p.p (\a.\b.a)) (p))) ((\p.p (\a.\b.a)) (p))) ((\a.\b.\t.t a b) (z) z))) n) (n) m) m)) n m)) ((\n.\s.\z.s (n s z)) (f ((\f.(\x.f (x x)) (\x.f (x x))) (\div.\n.\m.(\p.\t.\e.p t e) ((\n.\m.(\n.\m.(\n.n (\c.\a.\b.b) (\a.\b.a)) ((\n.\m.m (\n.\s.\z.(\p.p (\a.\b.b)) (n (\p.(\a.\b.\t.t a b) (s ((\p.p (\a.\b.a)) (p))) ((\p.p (\a.\b.a)) (p))) ((\a.\b.\t.t a b) (z) z))) n) (n) m)) (n) ((\n.\s.\z.(\p.p (\a.\b.b)) (n (\p.(\a.\b.\t.t a b) (s ((\p.p (\a.\b.a)) (p))) ((\p.p (\a.\b.a)) (p))) ((\a.\b.\t.t a b) (z) z))) (m))) (n) m) (\s.\z.z) ((\n.\s.\z.s (n s z)) (div ((\n.\m.m (\n.\s.\z.(\p.p (\a.\b.b)) (n (\p.(\a.\b.\t.t a b) (s ((\p.p (\a.\b.a)) (p))) ((\p.p (\a.\b.a)) (p))) ((\a.\b.\t.t a b) (z) z))) n) (n) m) m))) n m) m)) (\s.\z.z)) ((\p.p (\a.\b.b)) (list)) ((\i.(\f.(\x.f (x x)) (\x.f (x x))) (\f.\p.\i.(\p.\t.\e.p t e) ((\n.n (\c.\a.\b.b) (\a.\b.a)) (i)) p (f ((\p.(\f.(\x.f (x x)) (\x.f (x x))) (\f.\p.(\p.\t.\e.p t e) ((\p.(\f.(\x.f (x x)) (\x.f (x x))) (\f.\p.\i.(\p.\t.\e.p t e) ((\n.\m.(\n.n (\c.\a.\b.b) (\a.\b.a)) ((\n.\m.m (\n.\s.\z.(\p.p (\a.\b.b)) (n (\p.(\a.\b.\t.t a b) (s ((\p.p (\a.\b.a)) (p))) ((\p.p (\a.\b.a)) (p))) ((\a.\b.\t.t a b) (z) z))) n) (n) m)) (p) i) (\a.\b.a) ((\p.\t.\e.p t e) ((\n.n (\c.\a.\b.b) (\a.\b.a)) ((\f.(\x.f (x x)) (\x.f (x x))) (\mod.\n.\m.(\p.\t.\e.p t e) ((\n.\m.(\n.\m.(\n.n (\c.\a.\b.b) (\a.\b.a)) ((\n.\m.m (\n.\s.\z.(\p.p (\a.\b.b)) (n (\p.(\a.\b.\t.t a b) (s ((\p.p (\a.\b.a)) (p))) ((\p.p (\a.\b.a)) (p))) ((\a.\b.\t.t a b) (z) z))) n) (n) m)) (n) ((\n.\s.\z.(\p.p (\a.\b.b)) (n (\p.(\a.\b.\t.t a b) (s ((\p.p (\a.\b.a)) (p))) ((\p.p (\a.\b.a)) (p))) ((\a.\b.\t.t a b) (z) z))) (m))) (n) m) n (mod ((\n.\m.m (\n.\s.\z.(\p.p (\a.\b.b)) (n (\p.(\a.\b.\t.t a b) (s ((\p.p (\a.\b.a)) (p))) ((\p.p (\a.\b.a)) (p))) ((\a.\b.\t.t a b) (z) z))) n) (n) m) m)) p i)) (\a.\b.b) (f p ((\n.\s.\z.s (n s z)) (i))))) p (\s.\z.s (s z))) (p)) p (f ((\n.\s.\z.s (n s z)) (p)))) ((\n.\s.\z.s (n s z)) (p))) (p)) ((\n.\s.\z.(\p.p (\a.\b.b)) (n (\p.(\a.\b.\t.t a b) (s ((\p.p (\a.\b.a)) (p))) ((\p.p (\a.\b.a)) (p))) ((\a.\b.\t.t a b) (z) z))) (i)))) (\s.\z.s (s z)) i) ((\n.\s.\z.(\p.p (\a.\b.b)) (n (\p.(\a.\b.\t.t a b) (s ((\p.p (\a.\b.a)) (p))) ((\p.p (\a.\b.a)) (p))) ((\a.\b.\t.t a b) (z) z))) ((\p.p (\a.\b.a)) (list)))) | + | <tex>\lambda list.(\lambda f.(\lambda x.f (x x))</tex><tex> (\lambda x.f (x x)))</tex><tex> (\lambda f.\lambda n.\lambda m.(\lambda p.\lambda t.\lambda e.p t e)</tex><tex> ((\lambda n.n (\lambda c.\lambda a.\lambda b.b)</tex><tex> (\lambda a.\lambda b.a))</tex><tex> ((\lambda f.(\lambda x.f (x x))</tex><tex> (\lambda x.f (x x)))</tex><tex> (\lambda mod.\lambda n.\lambda m.(\lambda p.\lambda t.\lambda e.p t e)</tex><tex> ((\lambda n.\lambda m.(\lambda n.\lambda m.(\lambda n.n(\lambda c.\lambda a.\lambda b.b)</tex><tex> (\lambda a.\lambda b.a))</tex><tex> ((\lambda n.\lambda m.m (\lambda n.\lambda s.\lambda z.(\lambda p.p (\lambda a.\lambda b.b))</tex><tex> (n (\lambda p.(\lambda a.\lambda b.\lambda t.t a b)</tex><tex> (s ((\lambda p.p (\lambda a.\lambda b.a))</tex><tex> (p)))</tex><tex> ((\lambda p.p (\lambda a.\lambda b.a))</tex><tex> (p)))</tex><tex> ((\lambda a.\lambda b.\lambda t.t a b)</tex><tex> (z)</tex><tex> z))) n) (n)</tex><tex> m)) (n)</tex><tex> ((\lambda n.\lambda s.\lambda z.(\lambda p.p (\lambda a.\lambda b.b))</tex><tex> (n (\lambda p.(\lambda a.\lambda b.\lambda t.t a b)</tex><tex> (s ((\lambda p.p (\lambda a.\lambda b.a))</tex><tex> (p)))</tex><tex> ((\lambda p.p (\lambda a.\lambda b.a))</tex><tex> (p)))</tex><tex> ((\lambda a.\lambda b.\lambda t.t a b)</tex><tex> (z)</tex><tex> z))) (m)))</tex><tex> (n)</tex><tex> m) n (mod ((\lambda n.\lambda m.m (\lambda n.\lambda s.\lambda z.(\lambda p.p (\lambda a.\lambda b.b))</tex><tex> (n (\lambda p.(\lambda a.\lambda b.\lambda t.t a b)</tex><tex> (s ((\lambda p.p (\lambda a.\lambda b.a))</tex><tex> (p)))</tex><tex> ((\lambda p.p (\lambda a.\lambda b.a))</tex><tex> (p)))</tex><tex> ((\lambda a.\lambda b.\lambda t.t a b)</tex><tex> (z)</tex><tex> z))) n) (n)</tex><tex> m) m)) n m)) ((\lambda n.\lambda s.\lambda z.s (n s z))</tex><tex> (f ((\lambda f.(\lambda x.f (x x))</tex><tex> (\lambda x.f (x x)))</tex><tex> (\lambda div.\lambda n.\lambda m.(\lambda p.\lambda t.\lambda e.p t e)</tex><tex> ((\lambda n.\lambda m.(\lambda n.\lambda m.(\lambda n.n (\lambda c.\lambda a.\lambda b.b)</tex><tex> (\lambda a.\lambda b.a))</tex><tex> ((\lambda n.\lambda m.m (\lambda n.\lambda s.\lambda z.(\lambda p.p (\lambda a.\lambda b.b))</tex><tex> (n (\lambda p.(\lambda a.\lambda b.\lambda t.t a b)</tex><tex> (s ((\lambda p.p (\lambda a.\lambda b.a))</tex><tex> (p)))</tex><tex> ((\lambda p.p (\lambda a.\lambda b.a))</tex><tex> (p)))</tex><tex> ((\lambda a.\lambda b.\lambda t.t a b)</tex><tex> (z)</tex><tex> z))) n) (n)</tex><tex> m)) (n)</tex><tex> ((\lambda n.\lambda s.\lambda z.(\lambda p.p (\lambda a.\lambda b.b))</tex><tex> (n (\lambda p.(\lambda a.\lambda b.\lambda t.t a b)</tex><tex> (s ((\lambda p.p (\lambda a.\lambda b.a))</tex><tex> (p)))</tex><tex> ((\lambda p.p (\lambda a.\lambda b.a))</tex><tex> (p)))</tex><tex> ((\lambda a.\lambda b.\lambda t.t a b)</tex><tex> (z)</tex><tex> z))) (m)))</tex><tex> (n)</tex><tex> m) (\lambda s.\lambda z.z)</tex><tex> ((\lambda n.\lambda s.\lambda z.s (n s z))</tex><tex> (div ((\lambda n.\lambda m.m (\lambda n.\lambda s.\lambda z.(\lambda p.p (\lambda a.\lambda b.b))</tex><tex> (n (\lambda p.(\lambda a.\lambda b.\lambda t.t a b)</tex><tex> (s ((\lambda p.p (\lambda a.\lambda b.a))</tex><tex> (p)))</tex><tex> ((\lambda p.p (\lambda a.\lambda b.a))</tex><tex> (p)))</tex><tex> ((\lambda a.\lambda b.\lambda t.t a b)</tex><tex> (z)</tex><tex> z))) n) (n)</tex><tex> m) m))) n m) m)) (\lambda s.\lambda z.z))</tex><tex> ((\lambda p.p (\lambda a.\lambda b.b))</tex><tex> (list))</tex><tex> ((\lambda i.(\lambda f.(\lambda x.f (x x))</tex><tex> (\lambda x.f (x x)))</tex><tex> (\lambda f.\lambda p.\lambda i.(\lambda p.\lambda t.\lambda e.p t e)</tex><tex> ((\lambda n.n (\lambda c.\lambda a.\lambda b.b)</tex><tex> (\lambda a.\lambda b.a))</tex><tex> (i))</tex><tex> p (f ((\lambda p.(\lambda f.(\lambda x.f (x x))</tex><tex> (\lambda x.f (x x)))</tex><tex> (\lambda f.\lambda p.(\lambda p.\lambda t.\lambda e.p t e)</tex><tex> ((\lambda p.(\lambda f.(\lambda x.f (x x))</tex><tex> (\lambda x.f (x x)))</tex><tex> (\lambda f.\lambda p.\lambda i.(\lambda p.\lambda t.\lambda e.p t e)</tex><tex> ((\lambda n.\lambda m.(\lambda n.n (\lambda c.\lambda a.\lambda b.b)</tex><tex> (\lambda a.\lambda b.a))</tex><tex> ((\lambda n.\lambda m.m (\lambda n.\lambda s.\lambda z.(\lambda p.p (\lambda a.\lambda b.b))</tex><tex> (n (\lambda p.(\lambda a.\lambda b.\lambda t.t a b)</tex><tex> (s ((\lambda p.p (\lambda a.\lambda b.a))</tex><tex> (p)))</tex><tex> ((\lambda p.p (\lambda a.\lambda b.a))</tex><tex> (p)))</tex><tex> ((\lambda a.\lambda b.\lambda t.t a b)</tex><tex> (z)</tex><tex> z))) n) (n)</tex><tex> m)) (p)</tex><tex> i) (\lambda a.\lambda b.a)</tex><tex> ((\lambda p.\lambda t.\lambda e.p t e)</tex><tex> ((\lambda n.n (\lambda c.\lambda a.\lambda b.b)</tex><tex> (\lambda a.\lambda b.a))</tex><tex> ((\lambda f.(\lambda x.f (x x))</tex><tex> (\lambda x.f (x x)))</tex><tex> (\lambda mod.\lambda n.\lambda m.(\lambda p.\lambda t.\lambda e.p t e)</tex><tex> ((\lambda n.\lambda m.(\lambda n.\lambda m.(\lambda n.n (\lambda c.\lambda a.\lambda b.b)</tex><tex> (\lambda a.\lambda b.a))</tex><tex> ((\lambda n.\lambda m.m (\lambda n.\lambda s.\lambda z.(\lambda p.p (\lambda a.\lambda b.b))</tex><tex> (n (\lambda p.(\lambda a.\lambda b.\lambda t.t a b)</tex><tex> (s ((\lambda p.p (\lambda a.\lambda b.a))</tex><tex> (p)))</tex><tex> ((\lambda p.p (\lambda a.\lambda b.a))</tex><tex> (p)))</tex><tex> ((\lambda a.\lambda b.\lambda t.t a b)</tex><tex> (z)</tex><tex> z))) n) (n)</tex><tex> m)) (n)</tex><tex> ((\lambda n.\lambda s.\lambda z.(\lambda p.p (\lambda a.\lambda b.b))</tex><tex> (n (\lambda p.(\lambda a.\lambda b.\lambda t.t a b)</tex><tex> (s ((\lambda p.p (\lambda a.\lambda b.a))</tex><tex> (p)))</tex><tex> ((\lambda p.p (\lambda a.\lambda b.a))</tex><tex> (p)))</tex><tex> ((\lambda a.\lambda b.\lambda t.t a b)</tex><tex> (z)</tex><tex> z))) (m)))</tex><tex> (n)</tex><tex> m) n (mod ((\lambda n.\lambda m.m (\lambda n.\lambda s.\lambda z.(\lambda p.p (\lambda a.\lambda b.b))</tex><tex> (n (\lambda p.(\lambda a.\lambda b.\lambda t.t a b)</tex><tex> (s ((\lambda p.p (\lambda a.\lambda b.a))</tex><tex> (p)))</tex><tex> ((\lambda p.p (\lambda a.\lambda b.a))</tex><tex> (p)))</tex><tex> ((\lambda a.\lambda b.\lambda t.t a b)</tex><tex> (z)</tex><tex> z))) n) (n)</tex><tex> m) m)) p i)) (\lambda a.\lambda b.b)</tex><tex> (f p ((\lambda n.\lambda s.\lambda z.s (n s z))</tex><tex> (i)))))</tex><tex> p (\lambda s.\lambda z.s (s z)))</tex><tex> (p))</tex><tex> p (f ((\lambda n.\lambda s.\lambda z.s (n s z))</tex><tex> (p))))</tex><tex> ((\lambda n.\lambda s.\lambda z.s (n s z))</tex><tex> (p)))</tex><tex> (p))</tex><tex> ((\lambda n.\lambda s.\lambda z.(\lambda p.p (\lambda a.\lambda b.b))</tex><tex> (n (\lambda p.(\lambda a.\lambda b.\lambda t.t a b)</tex><tex> (s ((\lambda p.p (\lambda a.\lambda b.a))</tex><tex> (p)))</tex><tex> ((\lambda p.p (\lambda a.\lambda b.a))</tex><tex> (p)))</tex><tex> ((\lambda a.\lambda b.\lambda t.t a b)</tex><tex> (z)</tex><tex> z))) (i))))</tex><tex> (\lambda s.\lambda z.s (s z))</tex><tex> i) ((\lambda n.\lambda s.\lambda z.(\lambda p.p (\lambda a.\lambda b.b))</tex><tex> (n (\lambda p.(\lambda a.\lambda b.\lambda t.t a b)</tex><tex> (s ((\lambda p.p (\lambda a.\lambda b.a))</tex><tex> (p)))</tex><tex> ((\lambda p.p (\lambda a.\lambda b.a))</tex><tex> (p)))</tex><tex> ((\lambda a.\lambda b.\lambda t.t a b)</tex><tex> (z)</tex><tex> z))) ((\lambda p.p (\lambda a.\lambda b.a))</tex><tex> (list))))</tex> |
====tail==== | ====tail==== | ||
− | \list.(\a.\b.\t.t a b) ((\n.\s.\z.(\p.p (\a.\b.b)) (n (\p.(\a.\b.\t.t a b) (s ((\p.p (\a.\b.a)) (p))) ((\p.p (\a.\b.a)) (p))) ((\a.\b.\t.t a b) (z) z))) ((\p.p (\a.\b.a)) (list))) ((\f.(\x.f (x x)) (\x.f (x x))) (\f.\n.\m.(\p.\t.\e.p t e) ((\n.n (\c.\a.\b.b) (\a.\b.a)) ((\f.(\x.f (x x)) (\x.f (x x))) (\mod.\n.\m.(\p.\t.\e.p t e) ((\n.\m.(\n.\m.(\n.n (\c.\a.\b.b) (\a.\b.a)) ((\n.\m.m (\n.\s.\z.(\p.p (\a.\b.b)) (n (\p.(\a.\b.\t.t a b) (s ((\p.p (\a.\b.a)) (p))) ((\p.p (\a.\b.a)) (p))) ((\a.\b.\t.t a b) (z) z))) n) (n) m)) (n) ((\n.\s.\z.(\p.p (\a.\b.b)) (n (\p.(\a.\b.\t.t a b) (s ((\p.p (\a.\b.a)) (p))) ((\p.p (\a.\b.a)) (p))) ((\a.\b.\t.t a b) (z) z))) (m))) (n) m) n (mod ((\n.\m.m (\n.\s.\z.(\p.p (\a.\b.b)) (n (\p.(\a.\b.\t.t a b) (s ((\p.p (\a.\b.a)) (p))) ((\p.p (\a.\b.a)) (p))) ((\a.\b.\t.t a b) (z) z))) n) (n) m) m)) n m)) (f ((\f.(\x.f (x x)) (\x.f (x x))) (\div.\n.\m.(\p.\t.\e.p t e) ((\n.\m.(\n.\m.(\n.n (\c.\a.\b.b) (\a.\b.a)) ((\n.\m.m (\n.\s.\z.(\p.p (\a.\b.b)) (n (\p.(\a.\b.\t.t a b) (s ((\p.p (\a.\b.a)) (p))) ((\p.p (\a.\b.a)) (p))) ((\a.\b.\t.t a b) (z) z))) n) (n) m)) (n) ((\n.\s.\z.(\p.p (\a.\b.b)) (n (\p.(\a.\b.\t.t a b) (s ((\p.p (\a.\b.a)) (p))) ((\p.p (\a.\b.a)) (p))) ((\a.\b.\t.t a b) (z) z))) (m))) (n) m) (\s.\z.z) ((\n.\s.\z.s (n s z)) (div ((\n.\m.m (\n.\s.\z.(\p.p (\a.\b.b)) (n (\p.(\a.\b.\t.t a b) (s ((\p.p (\a.\b.a)) (p))) ((\p.p (\a.\b.a)) (p))) ((\a.\b.\t.t a b) (z) z))) n) (n) m) m))) n m) m) n) ((\p.p (\a.\b.b)) (list)) ((\i.(\f.(\x.f (x x)) (\x.f (x x))) (\f.\p.\i.(\p.\t.\e.p t e) ((\n.n (\c.\a.\b.b) (\a.\b.a)) (i)) p (f ((\p.(\f.(\x.f (x x)) (\x.f (x x))) (\f.\p.(\p.\t.\e.p t e) ((\p.(\f.(\x.f (x x)) (\x.f (x x))) (\f.\p.\i.(\p.\t.\e.p t e) ((\n.\m.(\n.n (\c.\a.\b.b) (\a.\b.a)) ((\n.\m.m (\n.\s.\z.(\p.p (\a.\b.b)) (n (\p.(\a.\b.\t.t a b) (s ((\p.p (\a.\b.a)) (p))) ((\p.p (\a.\b.a)) (p))) ((\a.\b.\t.t a b) (z) z))) n) (n) m)) (p) i) (\a.\b.a) ((\p.\t.\e.p t e) ((\n.n (\c.\a.\b.b) (\a.\b.a)) ((\f.(\x.f (x x)) (\x.f (x x))) (\mod.\n.\m.(\p.\t.\e.p t e) ((\n.\m.(\n.\m.(\n.n (\c.\a.\b.b) (\a.\b.a)) ((\n.\m.m (\n.\s.\z.(\p.p (\a.\b.b)) (n (\p.(\a.\b.\t.t a b) (s ((\p.p (\a.\b.a)) (p))) ((\p.p (\a.\b.a)) (p))) ((\a.\b.\t.t a b) (z) z))) n) (n) m)) (n) ((\n.\s.\z.(\p.p (\a.\b.b)) (n (\p.(\a.\b.\t.t a b) (s ((\p.p (\a.\b.a)) (p))) ((\p.p (\a.\b.a)) (p))) ((\a.\b.\t.t a b) (z) z))) (m))) (n) m) n (mod ((\n.\m.m (\n.\s.\z.(\p.p (\a.\b.b)) (n (\p.(\a.\b.\t.t a b) (s ((\p.p (\a.\b.a)) (p))) ((\p.p (\a.\b.a)) (p))) ((\a.\b.\t.t a b) (z) z))) n) (n) m) m)) p i)) (\a.\b.b) (f p ((\n.\s.\z.s (n s z)) (i))))) p (\s.\z.s (s z))) (p)) p (f ((\n.\s.\z.s (n s z)) (p)))) ((\n.\s.\z.s (n s z)) (p))) (p)) ((\n.\s.\z.(\p.p (\a.\b.b)) (n (\p.(\a.\b.\t.t a b) (s ((\p.p (\a.\b.a)) (p))) ((\p.p (\a.\b.a)) (p))) ((\a.\b.\t.t a b) (z) z))) (i)))) (\s.\z.s (s z)) i) ((\n.\s.\z.(\p.p (\a.\b.b)) (n (\p.(\a.\b.\t.t a b) (s ((\p.p (\a.\b.a)) (p))) ((\p.p (\a.\b.a)) (p))) ((\a.\b.\t.t a b) (z) z))) ((\p.p (\a.\b.a)) (list))))) | + | <tex>\lambda list.(\lambda a.\lambda b.\lambda t.t a b)</tex><tex> ((\lambda n.\lambda s.\lambda z.(\lambda p.p (\lambda a.\lambda b.b))</tex><tex> (n (\lambda p.(\lambda a.\lambda b.\lambda t.t a b)</tex><tex> (s ((\lambda p.p (\lambda a.\lambda b.a))</tex><tex> (p)))</tex><tex> ((\lambda p.p (\lambda a.\lambda b.a))</tex><tex> (p)))</tex><tex> ((\lambda a.\lambda b.\lambda t.t a b)</tex><tex> (z)</tex><tex> z))) ((\lambda p.p (\lambda a.\lambda b.a))</tex><tex> (list)))</tex><tex> ((\lambda f.(\lambda x.f (x x))</tex><tex> (\lambda x.f (x x)))</tex><tex> (\lambda f.\lambda n.\lambda m.(\lambda p.\lambda t.\lambda e.p t e)</tex><tex> ((\lambda n.n (\lambda c.\lambda a.\lambda b.b)</tex><tex> (\lambda a.\lambda b.a))</tex><tex> ((\lambda f.(\lambda x.f (x x))</tex><tex> (\lambda x.f (x x)))</tex><tex> (\lambda mod.\lambda n.\lambda m.(\lambda p.\lambda t.\lambda e.p t e)</tex><tex> ((\lambda n.\lambda m.(\lambda n.\lambda m.(\lambda n.n (\lambda c.\lambda a.\lambda b.b)</tex><tex> (\lambda a.\lambda b.a))</tex><tex> ((\lambda n.\lambda m.m (\lambda n.\lambda s.\lambda z.(\lambda p.p (\lambda a.\lambda b.b))</tex><tex> (n (\lambda p.(\lambda a.\lambda b.\lambda t.t a b)</tex><tex> (s ((\lambda p.p (\lambda a.\lambda b.a))</tex><tex> (p)))</tex><tex> ((\lambda p.p (\lambda a.\lambda b.a))</tex><tex> (p)))</tex><tex> ((\lambda a.\lambda b.\lambda t.t a b)</tex><tex> (z)</tex><tex> z))) n) (n)</tex><tex> m)) (n)</tex><tex> ((\lambda n.\lambda s.\lambda z.(\lambda p.p (\lambda a.\lambda b.b))</tex><tex> (n (\lambda p.(\lambda a.\lambda b.\lambda t.t a b)</tex><tex> (s ((\lambda p.p (\lambda a.\lambda b.a))</tex><tex> (p)))</tex><tex> ((\lambda p.p (\lambda a.\lambda b.a))</tex><tex> (p)))</tex><tex> ((\lambda a.\lambda b.\lambda t.t a b)</tex><tex> (z)</tex><tex> z))) (m)))</tex><tex> (n)</tex><tex> m) n (mod ((\lambda n.\lambda m.m (\lambda n.\lambda s.\lambda z.(\lambda p.p (\lambda a.\lambda b.b))</tex><tex> (n (\lambda p.(\lambda a.\lambda b.\lambda t.t a b)</tex><tex> (s ((\lambda p.p (\lambda a.\lambda b.a))</tex><tex> (p)))</tex><tex> ((\lambda p.p (\lambda a.\lambda b.a))</tex><tex> (p)))</tex><tex> ((\lambda a.\lambda b.\lambda t.t a b)</tex><tex> (z)</tex><tex> z))) n) (n)</tex><tex> m) m)) n m)) (f ((\lambda f.(\lambda x.f (x x))</tex><tex> (\lambda x.f (x x)))</tex><tex> (\lambda div.\lambda n.\lambda m.(\lambda p.\lambda t.\lambda e.p t e)</tex><tex> ((\lambda n.\lambda m.(\lambda n.\lambda m.(\lambda n.n (\lambda c.\lambda a.\lambda b.b)</tex><tex> (\lambda a.\lambda b.a))</tex><tex> ((\lambda n.\lambda m.m (\lambda n.\lambda s.\lambda z.(\lambda p.p (\lambda a.\lambda b.b))</tex><tex> (n (\lambda p.(\lambda a.\lambda b.\lambda t.t a b)</tex><tex> (s ((\lambda p.p (\lambda a.\lambda b.a))</tex><tex> (p)))</tex><tex> ((\lambda p.p (\lambda a.\lambda b.a))</tex><tex> (p)))</tex><tex> ((\lambda a.\lambda b.\lambda t.t a b)</tex><tex> (z)</tex><tex> z))) n) (n)</tex><tex> m)) (n)</tex><tex> ((\lambda n.\lambda s.\lambda z.(\lambda p.p (\lambda a.\lambda b.b))</tex><tex> (n (\lambda p.(\lambda a.\lambda b.\lambda t.t a b)</tex><tex> (s ((\lambda p.p (\lambda a.\lambda b.a))</tex><tex> (p)))</tex><tex> ((\lambda p.p (\lambda a.\lambda b.a))</tex><tex> (p)))</tex><tex> ((\lambda a.\lambda b.\lambda t.t a b)</tex><tex> (z)</tex><tex> z))) (m)))</tex><tex> (n)</tex><tex> m) (\lambda s.\lambda z.z)</tex><tex> ((\lambda n.\lambda s.\lambda z.s (n s z))</tex><tex> (div ((\lambda n.\lambda m.m (\lambda n.\lambda s.\lambda z.(\lambda p.p (\lambda a.\lambda b.b))</tex><tex> (n (\lambda p.(\lambda a.\lambda b.\lambda t.t a b)</tex><tex> (s ((\lambda p.p (\lambda a.\lambda b.a))</tex><tex> (p)))</tex><tex> ((\lambda p.p (\lambda a.\lambda b.a))</tex><tex> (p)))</tex><tex> ((\lambda a.\lambda b.\lambda t.t a b)</tex><tex> (z)</tex><tex> z))) n) (n)</tex><tex> m) m))) n m) m) n) ((\lambda p.p (\lambda a.\lambda b.b))</tex><tex> (list))</tex><tex> ((\lambda i.(\lambda f.(\lambda x.f (x x))</tex><tex> (\lambda x.f (x x)))</tex><tex> (\lambda f.\lambda p.\lambda i.(\lambda p.\lambda t.\lambda e.p t e)</tex><tex> ((\lambda n.n (\lambda c.\lambda a.\lambda b.b)</tex><tex> (\lambda a.\lambda b.a))</tex><tex> (i))</tex><tex> p (f ((\lambda p.(\lambda f.(\lambda x.f (x x))</tex><tex> (\lambda x.f (x x)))</tex><tex> (\lambda f.\lambda p.(\lambda p.\lambda t.\lambda e.p t e)</tex><tex> ((\lambda p.(\lambda f.(\lambda x.f (x x))</tex><tex> (\lambda x.f (x x)))</tex><tex> (\lambda f.\lambda p.\lambda i.(\lambda p.\lambda t.\lambda e.p t e)</tex><tex> ((\lambda n.\lambda m.(\lambda n.n (\lambda c.\lambda a.\lambda b.b)</tex><tex> (\lambda a.\lambda b.a))</tex><tex> ((\lambda n.\lambda m.m (\lambda n.\lambda s.\lambda z.(\lambda p.p (\lambda a.\lambda b.b))</tex><tex> (n (\lambda p.(\lambda a.\lambda b.\lambda t.t a b)</tex><tex> (s ((\lambda p.p (\lambda a.\lambda b.a))</tex><tex> (p)))</tex><tex> ((\lambda p.p (\lambda a.\lambda b.a))</tex><tex> (p)))</tex><tex> ((\lambda a.\lambda b.\lambda t.t a b)</tex><tex> (z)</tex><tex> z))) n) (n)</tex><tex> m)) (p)</tex><tex> i) (\lambda a.\lambda b.a)</tex><tex> ((\lambda p.\lambda t.\lambda e.p t e)</tex><tex> ((\lambda n.n (\lambda c.\lambda a.\lambda b.b)</tex><tex> (\lambda a.\lambda b.a))</tex><tex> ((\lambda f.(\lambda x.f (x x))</tex><tex> (\lambda x.f (x x)))</tex><tex> (\lambda mod.\lambda n.\lambda m.(\lambda p.\lambda t.\lambda e.p t e)</tex><tex> ((\lambda n.\lambda m.(\lambda n.\lambda m.(\lambda n.n (\lambda c.\lambda a.\lambda b.b)</tex><tex> (\lambda a.\lambda b.a))</tex><tex> ((\lambda n.\lambda m.m (\lambda n.\lambda s.\lambda z.(\lambda p.p (\lambda a.\lambda b.b))</tex><tex> (n (\lambda p.(\lambda a.\lambda b.\lambda t.t a b)</tex><tex> (s ((\lambda p.p (\lambda a.\lambda b.a))</tex><tex> (p)))</tex><tex> ((\lambda p.p (\lambda a.\lambda b.a))</tex><tex> (p)))</tex><tex> ((\lambda a.\lambda b.\lambda t.t a b)</tex><tex> (z)</tex><tex> z))) n) (n)</tex><tex> m)) (n)</tex><tex> ((\lambda n.\lambda s.\lambda z.(\lambda p.p (\lambda a.\lambda b.b))</tex><tex> (n (\lambda p.(\lambda a.\lambda b.\lambda t.t a b)</tex><tex> (s ((\lambda p.p (\lambda a.\lambda b.a))</tex><tex> (p)))</tex><tex> ((\lambda p.p (\lambda a.\lambda b.a))</tex><tex> (p)))</tex><tex> ((\lambda a.\lambda b.\lambda t.t a b)</tex><tex> (z)</tex><tex> z))) (m)))</tex><tex> (n)</tex><tex> m) n (mod ((\lambda n.\lambda m.m (\lambda n.\lambda s.\lambda z.(\lambda p.p (\lambda a.\lambda b.b))</tex><tex> (n (\lambda p.(\lambda a.\lambda b.\lambda t.t a b)</tex><tex> (s ((\lambda p.p (\lambda a.\lambda b.a))</tex><tex> (p)))</tex><tex> ((\lambda p.p (\lambda a.\lambda b.a))</tex><tex> (p)))</tex><tex> ((\lambda a.\lambda b.\lambda t.t a b)</tex><tex> (z)</tex><tex> z))) n) (n)</tex><tex> m) m)) p i)) (\lambda a.\lambda b.b)</tex><tex> (f p ((\lambda n.\lambda s.\lambda z.s (n s z))</tex><tex> (i)))))</tex><tex> p (\lambda s.\lambda z.s (s z)))</tex><tex> (p))</tex><tex> p (f ((\lambda n.\lambda s.\lambda z.s (n s z))</tex><tex> (p))))</tex><tex> ((\lambda n.\lambda s.\lambda z.s (n s z))</tex><tex> (p)))</tex><tex> (p))</tex><tex> ((\lambda n.\lambda s.\lambda z.(\lambda p.p (\lambda a.\lambda b.b))</tex><tex> (n (\lambda p.(\lambda a.\lambda b.\lambda t.t a b)</tex><tex> (s ((\lambda p.p (\lambda a.\lambda b.a))</tex><tex> (p)))</tex><tex> ((\lambda p.p (\lambda a.\lambda b.a))</tex><tex> (p)))</tex><tex> ((\lambda a.\lambda b.\lambda t.t a b)</tex><tex> (z)</tex><tex> z))) (i))))</tex><tex> (\lambda s.\lambda z.s (s z))</tex><tex> i) ((\lambda n.\lambda s.\lambda z.(\lambda p.p (\lambda a.\lambda b.b))</tex><tex> (n (\lambda p.(\lambda a.\lambda b.\lambda t.t a b)</tex><tex> (s ((\lambda p.p (\lambda a.\lambda b.a))</tex><tex> (p)))</tex><tex> ((\lambda p.p (\lambda a.\lambda b.a))</tex><tex> (p)))</tex><tex> ((\lambda a.\lambda b.\lambda t.t a b)</tex><tex> (z)</tex><tex> z))) ((\lambda p.p (\lambda a.\lambda b.a))</tex><tex> (list)))))</tex> |
− | |||
− | |||
− | |||
− | [ | + | == См. также == |
+ | *[[Неразрешимость задачи вывода типов в языке с зависимыми типами]] | ||
− | [http:// | + | ==Источники информации== |
+ | * Lectures on the Curry Howard - Isomorphism | ||
+ | *[https://github.com/shd/tt2014 Д. Штукенберг. Лекции] | ||
+ | *[http://en.wikipedia.org/wiki/Lambda-calculus Английская Википедия] | ||
+ | *[http://ru.wikipedia.org/wiki/%D0%9B%D1%8F%D0%BC%D0%B1%D0%B4%D0%B0-%D0%B8%D1%81%D1%87%D0%B8%D1%81%D0%BB%D0%B5%D0%BD%D0%B8%D0%B5 Русская Википедия] | ||
+ | *[http://worrydream.com/AlligatorEggs Игра про крокодилов] | ||
− | [ | + | [[Категория: Теория формальных языков]] |
+ | [[Категория: Теория вычислимости]] |
Текущая версия на 19:42, 4 сентября 2022
Лямбда-исчисление (англ. lambda calculus) — формальная система, придуманная в 1930-х годах Алонзо Чёрчем. Лямбда-функция является, по сути, анонимной функцией. Эта концепция показала себя удобной и сейчас активно используется во многих языках программирования.
Лямбда-исчисление
Определение: |
Лямбда-выражением (англ. где — множество всех строк над фиксированным алфавитом . | -term) называется выражение, удовлетворяющее следующей грамматике:
Пробел во втором правиле является терминалом грамматики. Иногда его обозначают как @, чтобы он не сливался с другими символами в выражении.
В первом случае функция является просто переменной. Во втором происходит аппликация (применение) одной функции к другой. Это аналогично вычислению функции-левого операнда на аргументе-правом операнде. В третьем — абстракция по переменной. В данном случае происходит создание функции одного аргумента с заданными именем аргумента и телом функции.
Рассмотрим, например,
-терм . Эта функция принимает аргумент и возвращает его неизменённым. Например, . Аналогично, .Еще примеры:
Иногда
-термы пишут по другому. Для краткости подряд идущие лямбды заменяют на одну. Например:Приоритет операций
- Аппликация:
- Абстракция забирает себе всё, до чего дотянется:
- Скобки играют привычную роль группировки действий
Свободные и связанные переменные
Связанными переменными называются все переменные, по которым выше в дереве разбора были абстракции. Все остальные переменные называются свободными.
Например, в
, и связана, а — свободна. А в в своём первом вхождении переменная свободна, а во втором — связана.Связанные переменные — это аргументы функции. То есть для функции они являются локальными.
Рассмотрим функции
и . В первой из них при взгляде на понятно, что она имеет отношение к переменной, по которой производилась абстракция. Если по одной и той же переменной абстракция производилась более одного раза, то переменная связана с самым поздним (самым нижним в дереве разбора) абстрагированием. Например, в , переменная связана с самой правой абстракцией по .α-эквивалентность
Определение: |
и замкнуто относительно следующих правил: | -эквивалентностью (англ. -equivalence) — называется наименьшее соотношение эквивалентности на такое что:
Функции и являются -эквивалентными,
а и — нет.
β-редукция
Определение: |
и замкнуто относительно следующих правил | -редукция (англ. -reduction) — это наименьшее соотношение на такое что
Определение: |
Через | обозначают сведение к с помощью одной -редукции. А через — за ноль или более.
В -редукции вполне возможна функция вида . Во время подстановки вместо внутренняя переменная не заменяется - действует принцип локальной переменной. Но принято считать, что таких ситуаций не возникает и все переменные называются разными именами.
Каррирование
Определение: |
Каррирование (англ. carrying) — преобразование функции от многих переменных в функцию, берущую свои аргументы по одному. Для функции | типа оператор каррирования выполняет преобразование . Таким образом берет аргумент типа и возвращает функцию типа . С интуитивной точки зрения, каррирование функции позволяет фиксировать ее некоторый аргумент, возвращая функцию от остальных аргументов. Таким образом, представляет собой функцию типа .
Нотация Де Брауна
Существует также альтернативное эквивалентное определение
-исчисления. В оригинальном определении для обозначения переменных использовались имена, и была проблема с тем, что не были запрещены одинаковые имена в разных абстракциях.От этой проблемы можно избавиться следующим образом. Вместо имени переменной будет храниться натуральное число — количество абстракций в дереве разбора, на которое нужно подняться, чтобы найти ту лямбду, с которой данная переменная связана. В данной нотации получаются несколько более простые определения свободных переменных и
-редукции.Грамматику нотации можно задать как:
Примеры выражений в этой нотации:
Standart | de Bruijn |
---|---|
$\lambda x.x$ | $\lambda .0$ |
$\lambda z.z$ | $\lambda .0$ |
$\lambda x. \lambda y.x$ | $\lambda . \lambda .1$ |
$\lambda x. \lambda y. \lambda s. \lambda z.x\ s\ (y\ s\ z)$ | $\lambda . \lambda . \lambda . \lambda .3\ 1(2\ 1\ 0)$ |
$(\lambda x.x\ x)(\lambda x.x\ x)$ | $(\lambda .0\ 0)(\lambda .0\ 0)$ |
$(\lambda x. \lambda x.x)(\lambda y.y)$ | $(\lambda .\lambda .0)(\lambda .0)$ |
Переменная называется свободной, если ей соответствует число, которое больше количества абстракций на пути до неё в дереве разбора.
При
-редукции же нужно будет ко всем свободным переменным заменяющего дерева при каждой замене прибавить число, равное разницы уровней раньше и сейчас. Это будет соответствовать тому, что эта переменная продолжит «держаться» за ту же лямбду, что и раньше.Нумералы Чёрча и программирование на -исчислении
Определение
Введём на основе лямбда-исчисления аналог натуральных чисел, основанный на идее, что натуральное число — это или ноль, или увеличенное на единицу натуральное число.
Каждое число будет функцией двух аргументов: какой-то функции и начального значения. Число
будет раз применять функцию к начальному значению и возвращать результат. Если такому "числу" дать на вход функцию и в качестве начального значения, то на выходе как раз будет ожидаемое от функции число: .+1
Функция, прибавляющая
к числу, должна принимать первым аргументом число. Но число — функция двух аргументов. Значит, эта функция должна принимать три аргумента: "число" , которое хочется увеличить, функция, которую надо будет раз применить, и начальное значение.
Здесь
— раз применённая к функция . Но нужно применить раз. Отсюда .Сложение
Сложение двух чисел похоже на прибавление единицы. Но только надо прибавить не единицу, а второе число.
раз применить к применённому раз к
Умножение
Умножение похоже на сложение, но прибавлять надо не единицу, а второе число. Или, в терминах нумералов Чёрча, в качестве применяемой несколько раз функции должна быть не
, а функция, применяющая раз .
Здесь
— функция, которая раз применит к тому, что дадут ей на вход. С помощью -редукции можно немного сократить эту формулу
Возведение в степень
It's a kind of magic
Логические значения
Функции двух аргументов, возвращающие первый и второй, соответственное, аргументы. Забавный факт:
. Эти функции сделаны такими для того, чтобы красиво написать функцию :
Если ей в качестве первого аргумента дадут
, то вернётся , иначе — .Стандартные функции булевой логики:
Ещё одной важной функцией является функция проверки, является ли число нулём:
Функция выглядит несколько странно.
- функция, которая независимо от того, что ей дали на вход, возвращает . Тогда, если в качестве будет дан ноль, то функция, по определению нуля, не выполнится ни разу, и будет возвращено значение по умолчанию . Иначе же функция будет запущено, и вернётся .Пара
Функция
принимает два значения и запаковывает их в пару так, чтобы к ним можно было обращаться по и . В и вместо в будет подставлено или , возвращающие, соответственно, первый и второй аргументы, то есть или , соответственно.Вычитание
В отличие от всех предыдущих функций, вычитание для натуральных чисел определено только в случае, если уменьшаемое больше вычитаемого. Положим в противном случае результат равным нулю. Пусть уже есть функция, которая вычитает из числа единицу. Тогда на её основе легко сделать, собственно, вычитание.
Это то же самое, что
раз вычесть единицу из .Осталось, собственно, функция для вычитания единицы. Однако, это не так просто, как может показаться на первый взгляд. Проблема в том, что, имея функцию, которую нужно применить для того, чтобы продвинуться вперёд, продвинуться назад будет проблематично. Если попробовать воспользоваться идеей о том, чтобы, начав от нуля, идти вперёд, и пройти на один шаг меньше, то будет не очень понятно, как же остановиться ровно за один шаг до конца. Для реализации вычитания единицы сделаем следующее.
раз выполним следующее: имея пару построим пару . Тогда после шагов во втором элементе пары будет записано число , которое и хочется получить.
Если вы ничего не поняли, не огорчайтесь. Вычитание придумал Клини, когда ему вырывали зуб мудрости. А сейчас наркоз уже не тот.
Сравнение
Так как вычитание определено таким способом, чтобы для случая, в котором уменьшаемое больше, чем вычитаемое, возвращать ноль, можно определить сравнение на больше-меньше через него. Равными же числа
и считаются, если .
Комбинатор неподвижной точки
Попробуем выразить в лямбда-исчислении какую-нибудь функцию, использующую рекурсию. Например, факториал.
Мы столкнулись с проблемой. В определении функции
используется функция . При формальной замене, получим бесконечную функцию. Можно попытаться решить эту проблему следующим образом
Определение: |
Неподвижной точкой лямбда-функции | назовём такую функцию , что .
Лямбда исчисление обладаем замечательным свойством: у каждой функции есть неподвижная точка!
Рассмотрим следующую функцию.
Заметим, что
. Или, что то же самое,Рассмотрим функцию
Как было показано выше,
, то есть, , где — искомая функция, считающая факториал.
Это даст функцию, которая посчитает факториал числа. Но делать она это будет мееедленно-меееедленно. Для того, чтобы посчитать
потребовалось сделать 66066 -редукций.Наиболее известным комбинатором неподвижной точки является
-комбинатор, введенный известным американским ученым Хаскеллом Карри какДеление
Воспользовавшись идеей о том, что можно делать рекурсивные функции, сделаем функцию, которая будет искать частное двух чисел.
И остатка от деления
Проверка на простоту
— принимает число, которое требуется проверить на простоту и то, на что его надо опытаться поделить, перебирая это от до . Если на что-нибудь разделилось, то число — составное, иначе — простое.
Следующее простое число.
— следующее, больше либо равное заданного, — следующее, большее заданного.
пропрыгает простых чисел вперёд. принимает число и пропрыгивает столько простых чисел вперёд, начиная с двойки.
...и всего через 314007
-редукций вы узнаете, что третье простое число — семь!Списки
Для работы со списками чисел нам понадобятся следующие функции:
- — возвращает пустой список
- — принимает первый элемент и оставшийся список, склеивает их
- — вернуть голову списка
- — вернуть хвост списка
Список будем хранить в следующем виде:
. При этом, голова списка будет храниться как показатель степени при .
Выводы
На основе этого всего уже можно реализовать эмулятор машины тьюринга: с помощью пар, списков чисел можно хранить состояния. С помощью рекурсии можно обрабатывать переходы. Входная строка будет даваться, например, закодированной аналогично списку: пара из длины и числа, характеризующего список степенями простых. Я бы продолжил это писать, но уже на операции
я не дождался окончания выполнения. Скорость лямбда-исчисления как вычислителя печальна.Примеры (слабонервным не смотреть)
fact
head
tail
См. также
Источники информации
- Lectures on the Curry Howard - Isomorphism
- Д. Штукенберг. Лекции
- Английская Википедия
- Русская Википедия
- Игра про крокодилов