ТМВ-2020-Семинар-10.04.2020

Материал из Кафедра Прикладной Математики
Перейти к навигации Перейти к поиску

$$\def \q {\operatorname}$$ $$\def \w {\underline}$$ $$\def \l {\lambda}$$

$$\lambda$$–исчисление

Весь теоретический материал находится в лекциях №7 ($$\l$$-исчисление) и №8 ($$\l$$-моделирование).

Функция вычитания единицы

Вспомним из лекций, что мы вводили вспомогательную функцию $$g$$ следующим образом: $$g=\lambda p.\text{pair}(f(\text{fst }p))(\text{fst }p)$$.

Определим $$gf=\lambda f.g=\lambda fp.\text{pair}(f(\text{fst }p))(\text{fst }p)$$.

Тогда $$\operatorname{pre} =\lambda nfx.\text{snd}(n\ (gf\ f)\ (\text{pair }x\ x))$$.

Логические функции, $$\text{if}$$

$$\text{True}=\lambda x_1 x_2.x_1$$, $$\text{False}=\lambda x_1 x_2.x_2$$.

Основываясь на этих функциях определим функцию $$\text{if}$$:

$$\operatorname{if}=\lambda c\ t\ e.c\ t\ e $$.

$$\text{True}\ A\ C=((\lambda x_1 x_2.x_1) A) C \xrightarrow{\beta} (\lambda x_2.A)C \xrightarrow{\beta} \left[{C}/{x_2}\right]A=A$$

Функция $$\mbox{reverse}$$ элементов пары

Напомним: $$\operatorname{pair } \lambda xyf.f~x~y$$, $$\operatorname{pair}x~y=\lambda f.f~x~y$$.

$$\q{reverse}{(x,y)}=(y,x)$$
$$\q{reverse}=\lambda p.\q{pair}{(\q{snd}p)(\q{fst}p)}$$

Функции сравнения нумералов

Напомним: $$\underline{0}=\lambda fx.x $$, $$\w{1}=\lambda fx. f~x$$, $$\w{3}=\lambda fx.f~(f~x)$$ и т. д.
$$\q{isZero}=\l n.n~(\l z.\q{False})\q{True}$$

Определим предикаты сравнения:
$$«{\leqslant}»=\l xy.\q{isZero}{(\q{minus} x~y)}$$
$$«{<}»=«{\leqslant}»~x~(\q{pre}y)$$
$$«{=}»=\l xy.\q{and}{(«{\leqslant}»~x~y)~(«{\leqslant}»~y~x)}$$

Рекурсивные функции

Построим $$\l$$-функции для некоторых рекурсивно определённых функций.

Рекурсивное определение $$\l$$-функция
$${\q{fact}=\begin{cases} 1 & x=0 \\ x\cdot\q{fact}{(x-1)} & x > 0 \end{cases} }$$ $$\q{fact}=\l x.(\q{isZero}x)~\w{1}~(\q{mult}{x~(\q{fact}{(\q{pre}x}))})$$
$${\q{div}=\begin{cases} 0 & n < m \\ 1+\q{div}{(n-m,m)} & n \geqslant m \end{cases} }$$ $$\q{div}=\l n m . («{<}»~{n~m})~\w{0}~(\q{succ}{(\q{div}{(\q{minus}{n~m})}~m)}) $$
$${\q{mod}=\begin{cases} n & n < m \\ \q{mod}{(n-m,m)} & n \geqslant m \end{cases} }$$ $$ \q{mod}=\l n m . («{<}»~{n~m})~n~(\q{mod}{(\q{minus}{n~m})}~m)$$
$$\q{fib}{(x)}=\begin{cases} 1 & x=\{0,1\} \\ \q{fib}{(n-1)}+\q{fib}{(n-2)} & x > 1 \end{cases} $$ $$\q{fib}=\l n.(«{<}»~{n~\w{1}})~(\q{add} { ( \q{fib} { ( \q{pre}{n} ) } ) ~ ( \q{fib} { ( \q{pre}{ ( \q{pre}{n} ) } ) } ) } ) $$

Также для функции нахождения числа Фибоначчи можно использовать следующую альтернативную конструкцию:

$$ \q{fib}=\l n . \q{fibRec}{\w{1}~\w{1}~n} \\ \q{fibRec}= \l a b n.(«{<}»~{n~\w{1}})~a~(\q{fibRec}{ (\q{add}{a~b})~a~(\q{pre}{n}) }) $$

Функции работы со списком*

* Некоторые функции в этом разделе некорректны. Смотри подробнее материалы семинара №9 ($$\lambda$$-моделирование. Работа со списком.)

Определим список как пару: $$\q{list}=\langle \q{head},\q{tail} \rangle$$

Собственно функция списка: $$\q{list}=\l h t f x.f h t $$

Пустой список, предикат пустоты списка

$$\q{empty}=\l h t f x.x $$ $$\q{isEmpty}=\l l.(\l x y . \q{False})~\q{True} $$

Проверим корректность предиката на примерах пустого списка и списка из одного элемента:
$$\q{isEmpty}{\q{empty}}=\l f x . x~(\l x y.\q{False})\q{True}=\q{True} $$
$$\q{isEmpty}{(\q{list}{\w{1}~\q{empty}})}=(\l f x . f ~\w{1} ~ \q{empty})~(\l x y.\q{False})~\q{True}=(\l x y.\q{False})~\w{1}~\q{empty}=\q{False} $$

Функции длины и «хвоста» списка

Определим функцию, возвращающая «хвост» списка и проверим её на примерах пустого списка и списка из одного элемента:
$$\q{tail}=\l l .l~\q{False}{\q{empty}} $$
$$\q{tail}\q{empty}=\q{empty}\q{False}\q{empty}=(\l f x . x)\q{False}\q{empty}=\q{empty} $$
$$\q{tail}{(\q{list}\w{1}\q{empty})}=\color{blue}{\|\q{list}\w{1}\q{empty}=\l f x . f~\w{1}~\q{empty}\|}=(\l f x . f~\w{1}~\q{empty})\q{False}\q{empty}=\q{False}\w{1}\q{empty}=(\l x_1 x_2 . x_2)~\w{1}~\q{empty}=\q{empty} $$

Определим рекурсивно функцию, возвращающую длину списка:
$$ \q{len}{l}= \begin{cases} 0 & l = \q{empty} \\ 1+\q{len}{(\q{tail})} & \text{иначе} \end{cases} $$

Получим следующую $$\l$$-функцию: $$\q{len}=\l l. l ~(\q{succ} {( \q {len} {( \q{tail} {l} )} )}) ~\w{0} $$