1632
правки
Изменения
м
{{В разработке}} '''Лямбда-исчисление'''(''англ. lambda calculus'') {{---}} формальная система, придуманная в 1930-х годах
Более формально, ''лямбда-функцию'' (или, ''лямбда-терм'') можно задать
следующей грамматикой:
Ещё один пример функцииЕще примеры:: <tex>x\\(x\operatorname{sum} = z)\\(\lambda x.(x\ z))\\(\lambda z.(\ lambda w.((\lambda y.((\ lambda x.(x\ z))\ x + y))\ w)))\\ </tex>. Эта функция двух аргументов,которая возвращает их суммуИногда <tex>\lambda</tex> -термы пишут по другому. Правда, здесь мы немного вышли за написанную выше грамматикуДля краткости подряд идущие лямбды заменяют на одну.Например:Ну да ладно. :<tex>\operatorname{sum}lambda x\ .\ \lambda y\ .P\ 2\ 3 to\equiv 5\lambda xy.P</tex>
Функции, получающиеся одна из другой с помощью <tex>\alpha</tex>-конверсий, называются
''<tex>\alpha</tex>-эквивалентными'' и обозначаются <tex>f \equiv_\alpha g</tex>.
* :<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>
Тут правда ничего не понятно? Наиболее известным комбинатором неподвижной точки является <tex>Y</tex>-комбинатор, введенный известным американским ученым Хаскеллом Карри как:'<tex>Y\ = \ \lambda f.(\lambda x.f(x\ x))\ (\lambda x.f(x\ x))</tex>
rollbackEdits.php mass rollback
Алонзо Чёрчем. Лямбда-функция является, по сути, анонимной функцией.
Эта концепция показала себя удобной и сейчас активно используется во многих
== Лямбда-исчисление==
{{Определение
|definition=
'''Лямбда-выражением''' (англ. <tex>\lambda</tex>''-term'') называется выражение, удовлетворяющее следующей грамматике:<br>
<tex>
\begin{array}{r c l}Lambda \langle Term to V\rangle & ::= & \langle Variable \rangle Lambda \to \ & | & Lambda \langle Term \rangle Lambda\langle Term \rangle \Lambda \ & | & to \lambda \langle Variable \rangle\ V .\ \langle Term \rangle\\ & | & ( \langle Term \rangle )\\\langle Variable \rangle & ::= & \langle Char \rangle +\\\end{array}Lambda
</tex>
где <tex>V</tex> {{---}} множество всех строк над фиксированным алфавитом <tex> \Sigma \setminus \{ "\lambda", "\ ",\ "."\} </tex>.
}}
Пробел во втором правиле является терминалом грамматики. Иногда его обозначают как @, чтобы он не сливался с другими символами в выражении.
В первом случае функция является просто переменной.
создание функции одного аргумента с заданными именем аргумента и телом функции.
Рассмотрим, например, функцию <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>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\ .\ x</tex>, <tex>x</tex> и связана, а <tex>y</tex>{{---}} свободна. А в <tex>\lambda y\ .\ x \ (\lambda x\ .\ x)</tex>
в своём первом вхождении переменная <tex>x</tex> свободна, а во втором {{---}} связана.
Связанные переменные {{---}} это аргументы функции. То есть для функции они являются локальными.
Рассмотрим функции <tex>\lambda y\ .\ y</tex> и <tex>\lambda x\ .\ y</tex>. В первой из них при взгляде на <tex>y</tex>
по <tex>x</tex>.
===α-конверсияэквивалентность=== Рассмотрим функции <tex>(\lambda x\ .\ x) z</tex> и <tex>(\lambda y\ .\ y) z</tex>. Интуитивно понятно, что они являются одинаковыми.
{{Определение
|definition='''<tex>\alpha</tex>-конверсияэквивалентностью'' {{---}} переименование связанной переменной' (англ. Выражение''<tex>\lambda x\ .\ falpha</tex> можно заменить -equivalence'') {{---}} называется наименьшее соотношение эквивалентности на <tex>\lambda y\ .\ f[x := y]Lambda</tex>, если такое что::<tex>yP=_\alpha P</tex> не входит свободно в для любого <tex>fP</tex>,где :<tex>f\lambda x.P=_\alpha \lambda y.P[x:=y]</tex> означает замену всех свободных вхождений если <tex>xy \not\in FV(P)</tex> в и замкнуто относительно следующих правил::<tex>f</tex> на <tex>yP=_\alpha P' \Rightarrow \forall x \in V: \lambda x.P=_\alpha \lambda x.P'\\P=_\alpha P' \Rightarrow \forall Z \in \Lambda : P Z =_\alpha P'Z\\P=_\alpha P' \Rightarrow \forall Z \in \Lambda : Z P =_\alpha Z P'\\P=_\alpha P' \Rightarrow P'=_\alpha P\\P=_\alpha P' \ \& \ P'=_\alpha P'' \Rightarrow P=_\alpha P''\\</tex>.
}}
Функции <tex>\lambda x\ .\ \lambda y\ .\ x\ y\ z</tex> и <tex>\lambda a\ .\ \lambda x\ .\ a\ x\ z</tex> являются <tex>\alpha</tex>-эквивалентными,
{{Определение
|definition=
'''<tex>\beta</tex>-редукция олицетворяет идею счёта значения функции''' (англ. Выражение вида ''<tex>(\lambda x\ .\ f)\ ybeta</tex> можно заменить -reduction'') {{---}} это наименьшее соотношение на <tex>f[x := y]\Lambda</tex>, где такое что:<tex>f(\lambda x.P)Q\to _\beta P[x:=yQ]</tex>, как и ранее, означаетзамкнуто относительно следующих правилзамену всех свободных вхождений :<tex>P\to _\beta P' \Rightarrow \forall x\in V:\lambda x.P\to _\beta \lambda x.P'\\P\to _\beta P' \Rightarrow \forall Z\in \Lambda : P\ Z\to _\beta P'\ Z\\P\to _\beta P' \Rightarrow \forall Z\in \Lambda : Z\ P\to _\beta Z\ P'</tex> в <tex>f</tex> на <tex>y</tex>.
}}
}}
В <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>\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)$
|}
Переменная называется свободной, если ей соответствует число, которое больше
При <tex>\beta</tex>-редукции же нужно будет ко всем свободным переменным заменяющего
дерева при каждой замене прибавить число, равное разницы уровней раньше и сейчас.
Это будет соответствовать тому, что эта переменная продолжит <<держаться>> «держаться» за
ту же лямбду, что и раньше.
число.
Каждое число будет функцией двух аргументов: какой-то функции и начального значения.
Число <tex>n</tex> будет <tex>n</tex> раз применять функцию к начальному значению и возвращать
результат. Если такому <<"числу>> " дать на вход функцию <tex>(+1)</tex> и <tex>0</tex> в качестве
начального значения, то на выходе как раз будет ожидаемое от функции число:
<tex>\bar 3\ (+1)\ 0 \equiv 3</tex>.
===+1===
Функция, прибавляющая <tex>1 </tex> к числу, должна принимать первым аргументом число.
Но число {{---}} функция двух аргументов. Значит, эта функция должна принимать три
аргумента: <<"число>> " <tex>n</tex>, которое хочется увеличить, функция, которую надо будет
<tex>n+1</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>
===Умножение===
функции должна быть не <tex>s</tex>, а функция, применяющая <tex>n</tex> раз <tex>s</tex>.
<tex>\operatorname{mult} = \lambda n\ .\ \lambda m\ .\ \lambda s\ .\ \lambda z\ .\ n\ (m\ s)\ z</tex>
Здесь <tex>m\ s</tex> {{---}} функция, которая <tex>m</tex> раз применит <tex>s</tex> к тому, что дадут ей на
It's a kind of magic
<tex>\operatorname{power} = \lambda n\ .\ \lambda m\ .\ \lambda s\ .\ \lambda z\ .\ m\ n\ s\ z</tex>
<tex>(\operatorname{power}\ \bar 3\ (\operatorname{succ}\ \bar 3))\ (+1)\ 0 \equiv 81</tex>
Стандартные функции булевой логики:
<tex>\operatorname{and} = \lambda n\ .\ \lambda m\ .\ \operatorname{if} \ n\ m\ \operatorname{false}</tex>
<tex>\operatorname{or} = \lambda n\ .\ \lambda m\ .\ \operatorname{if} \ n\ \operatorname{true} \ m</tex>
<tex>\operatorname{not} = \lambda b\ .\ \operatorname{if} \ b\ \operatorname{false} \ \operatorname{true}</tex>
Ещё одной важной функцией является функция проверки, является ли число нулём:
<tex>\operatorname{isZero} = \lambda n\ .\ n\ (\lambda c\ .\ \operatorname{false})\ \operatorname{true}</tex>
Функция выглядит несколько странно. <tex>\lambda c -> \to \operatorname{false}</tex> {{---}} функция, которая независимо
от того, что ей дали на вход, возвращает <tex>\operatorname{false}</tex>. Тогда, если в качестве <tex>n</tex>
будет дан ноль, то функция, по определению нуля, не выполнится ни разу, и будет
Осталось, собственно, функция для вычитания единицы. Однако, это не так просто, как может показаться на первый взгляд. Проблема в том, что, имея функцию, которую нужно применить для того, чтобы продвинуться вперёд, продвинуться назад будет проблематично. Если попробовать воспользоваться идеей о том, чтобы, начав от нуля, идти вперёд, и пройти на один шаг меньше, то будет не очень понятно, как же остановиться ровно за один шаг до конца. Для реализации вычитания единицы сделаем следующее. <tex>n</tex> раз выполним следующее: имея пару <tex>\langle n-1, n-2\rangle</tex> построим пару <tex>\langle n, n-1\rangle</tex>. Тогда после <tex>n</tex> шагов во втором элементе пары будет записано число <tex>n-1</tex>, которое и хочется получить.
<tex>\operatorname{pred} = \lambda n\ .\ \lambda s\ .\ \lambda z \to.\ \operatorname{snd} \ (
n\ (
\lambda p\ .\ \operatorname{pair}\ (s\ (\operatorname{fst} p))\ (\operatorname{fst} p)
)\ (\operatorname{pair}\ z\ z))</tex>
Если вы ничего не поняли, не огорчайтесь. Вычитание придумал Клини, когда ему вырывали зуб мудрости. А сейчас наркоз уже не тот.
===Комбинатор неподвижной точки===
Попробуем выразить в лямбда-исчислении какую-нибудь функцию, использующую рекурсию. НапрмерНапример, факториал.
<tex>\operatorname{fact} = \lambda x\ .\ \operatorname{if}\ (\operatorname{isZero}\ x)\ \bar 1\ (\operatorname{fact}\ (\operatorname{pred}\ x))</tex>
<tex>\operatorname{fact} = \operatorname{fix}\ \operatorname{fact'}</tex>
Это даст функцию, которая посчитает факториал числа. Но делать она это будет мееедленно-меееедленно. Для того, чтобы посчитать <tex?>5!</tex> потребовалось сделать 66066 <tex>\beta</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>
====fact====
<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====
<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====
<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))))) ==Ссылки==[http://en.wikipedia.org/wiki</Lambda-calculus Английская Википедия]tex>
== См. также ==*[[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 Русская ВикипедияНеразрешимость задачи вывода типов в языке с зависимыми типами]]
==Источники информации==* Lectures on the Curry Howard - Isomorphism*[https://github.com/shd/tt2014 Д. Штукенберг. Лекции]*[http://rainen.ifmowikipedia.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:/~komarov/Turingworrydream.lhs Тут можно это всё потыкатьcom/AlligatorEggs Игра про крокодилов]
[http[Категория://worrydream.com/AlligatorEggs А это игра про крокодильчиковТеория формальных языков]][[Категория: Теория вычислимости]]
