Изменения

\usepackage[english,russian]{babel}\usepackage[T2A]{fontenc}\usepackage[utf8]{inputenc}\usepackage{graphicx}\usepackage{expdlist}\usepackage{mfpic}\usepackage{comment}\usepackage{listings}\usepackage{epigraph}\usepackage{url}\usepackage{array}%include polycode.fmt%options ghci%format Var v = v%format App x y = x "\times" y%format `App` = " \cdot "%format Lam x = "\lambda" x "\to"%format if' = if%format then' = then%format else' = else%format $ = " " \long\def\ignore#1{} \begin{document} \ignore{\begin{code}import Prelude hiding (id, succ, pred, and, or, catch, head, tail)import qualified Prelude as P\end{code}} \ignore{\begin{code}import Control.Exceptionimport Control.Monad.Stateimport qualified Data.Map as Mimport Data.Maybe (fromMaybe) type Variable = Stringdata Term = Var Variable | Lam Variable Term | App Term Term deriving (Ord) instance Show Term where show (Var x) = x show (Lam x e) = "\\" ++ x ++ "." ++ show e show (App e1@(Lam _ _) e2) = "(" ++ show e1 ++ ") (" ++ show e2 ++ ")" show (App e1 (Var v)) = show e1 ++ " " ++ v show (App e1 e2) = show e1 ++ " (" ++ show e2 ++ ")" free (Var v) = [ v ]free (Lam v t) = filter (/= v) . free $ tfree (App t t') = (free t) ++ (free t') subst :: Term Лямбда-> Variable -> Term -> Termsubst t@(Var v) var what = if v == var then what else tsubst t@(Lam v b) var what = if v == var then t else Lam v (subst b var what)subst (App t t') var what = App (subst t var what) (subst t' var what) newname :: [Variable] -> Variable -> Variable newname fv = P.head . filter (not . flip elem fv) . iterate ('_':) deny:: [String] -> Term -> Termdeny d (Var v) = Var v -- Var $ newname d vdeny d (Lam v t) = Lam v' $ subst t v (Var v') where v' = newname (d ++ free t) vdeny d (App t1 t2) = App (deny d t1) (deny d t2) unifyBound :: Term -> Term unifyBound e = fst $ runState (unifyBound' e) (M.empty, free e) unifyBound' :: Term -> State (M.Map Variable Variable, [Variable]) TermunifyBound' (Var v) = do (m, used) <- get return $ Var $ fromMaybe v (M.lookup v m)unifyBound' e@(App t1 t2) = do t1' <- unifyBound' t1 t2' <- unifyBound' t2 return $ App t1' t2исчисление'unifyBound' (Lam x t) = do (m, used) <- get let new = fst $ runState unused used put (M.insert x new m, new:used) e <- unifyBound' t (_, used') <- get put (m, used') return $ Lam new e eq :: Term -> Term -> Booleq (Var v) (Var v') = v == v'eq (Lam v1 e1) (Lam v2 e2) = v1 == v2 && e1 `eq` e2eq (App e1 e2) (App e1' e2') = e1 `eq` e1' && e2 `eq` e2'eq _ _ = False instance Eq Term where e1 == e2 = free e1 == free e2 && newE1 `eq` newE2 where newE1 = unifyBound e1 newE2 = unifyBound e2 fv = free e1 unused :: State [Variable] Variableunused = do used <- get let new = P.head $ filter (not . (`elem` used)) $ map show [1..] put $ new:used return new  no :: Integer -> Term -> Term no n t = no' n ({- unifyBound -} t) no' 0 t = error $ "Too long sequence at [" ++ show t ++ "]"no' n t | reduced = no (n - 1) rest | otherwise = t where (reduced, rest) = noOne t noOne :: Term -> (Bool, Term)noOne (App (Lam v t1) t2) = (True, subst (deny (free t2) t1) v t2)noOne t@(Var v) = (False, t)noOne (Lam v t) = (reduced, Lam v rest) where (reduced, rest) = noOne t noOne t@(App t1 t2) = if reducedLeft then (True, App t1' t2) else if reducedRight then (True, App t1 t2') else (False, t) where (reducedLeft, t1') = noOne t1 (reducedRight, t2') = noOne t2 fv = free t2 sa n t = sa' n $ {- unifyBound -} t sa' 0 t = error $ "Too long sequence at [" ++ show t ++ "]"sa' n t | reduced = sa (n - 1) rest | otherwise = t where (reduced, rest) = saOne t  saOne :: Term -> (Bool, Term)saOne t@(Var v) = (False, t)saOne (Lam v t) = (reduced, Lam v rest) where (reduced, rest) = saOne tsaOne t@(App t1 t2) = if reducedRight then (True, App t1 t2') else case t1 of (Lam v t1'') -> (True, subst (deny (free t2) t1'') v t2) where (_, t1''') = saOne t1'' _ -> (reducedLeft, App t1' t2) where (reducedRight, t2') = saOne t2 (reducedLeft, t1') = saOne t1 normIO :: Int -> Term -> IO TermnormIO step t = do let (reduced, rest) = noOne t print $ "================" ++ " step " ++ show step ++ " ======== " if reduced then normIO (step + 1) rest else do print rest return rest norm :: Term -> Termnorm = no 1000 toInt :: Term -> InttoInt (Var v) = 0toInt (Lam v x) = toInt xtoInt (App v1 v2) = (toInt v1) + (toInt v2) + 1 \end{code}}  \section{Лямбда-исчисление} \emph{Лямбда-исчисление}~--- формальная система, придуманная в 1930-х годах

Более формально, \emph{''лямбда-функцию} '' (или, \emph{''лямбда-терм}'') можно задать

Во втором происходит \emph{''аппликация} '' (\emph{''применение}'') одной функции к другой.

В третьем~{{--- \emph{}} ''абстракция} '' по переменной. В данном случае происходит

Рассмотрим, например, функцию |<tex>id = \lambda x \to x -</tex> x|. Эта функция принимает аргумент и

|<tex>id 2 == | \eval{id equiv 2}</tex>. Аналогично, |<tex>id y == y|</tex>.

Ещё один пример функции: |<tex>sum = \lambda x -> \to \lambda y -> \to x + y|. Эта функция двух аргументов,

Ну да ладно. |<tex>sum 2 3 == 5|</tex>

\subsection{===Приоритет операций}\begin{itemize}===\item * Применение левоассоциативно: |<tex>x y z w == ((x y) z) w|</tex>\item * Аппликация забирает себе всё, до чего дотянется:<tex>\lambda x \ |to \x -> lambda y \y -> to \lambda z -> \to z y x == \equiv \lambda x -> \to (\lambda y -> \to (\lambda z -> \to ((z y) x)))|</tex>\item * Скобки играют привычную роль группировки действий\end{itemize}

\subsection{===Свободные и связанные переменные}===\emph{''Связанными} '' переменными называются все переменные, по которым выше в

Например, в |<tex>\lambda x -> \to \lambda y -\to x</tex> x|, |<tex>x| </tex> связана, а |<tex>y|~</tex>{{--- }} свободна. А в |<tex>\lambda y -> \to x (\lambda x -> \to x)|</tex>в своём первом вхождении переменная |<tex>x| </tex> свободна, а во втором~{{--- }} связана.

Рассмотрим функции |<tex>\lambda y -\to y</tex> y| и |<tex>\lambda x -\to y</tex> y|. В первой из них при взгляде на |<tex>y|</tex>

|<tex>\lambda x -> \to \lambda x -> \to \lambda y -> \to \lambda x \to x -</tex> x|, переменная |<tex>x| </tex> связана с самой правой абстракцией по |<tex>x|</tex>.

\subsection{$===<tex>\alpha$</tex>-конверсия}===

Рассмотрим функции |<tex>(\lambda x -> \to x) z| </tex> и |<tex>(\lambda y -> \to y) z|</tex>. Интуитивно понятно, что они

\emph{${Определение|definition=''<tex>\alpha$</tex>-конверсия}~'' {{--- }} переименование связанной переменной. Выражение|<tex>\lambda x -\to f</tex> f| можно заменить на |<tex>\lambda y -> \to f[x := y]|</tex>, если |<tex>y| </tex> не входит свободно в |<tex>f|</tex>,где $<tex>f[x:=y]$ </tex> означает замену всех свободных вхождений $<tex>x$ </tex> в $<tex>f$ </tex> на $<tex>y$</tex>.

Функции, получающиеся одна из другой с помощью $<tex>\alpha$</tex>-конверсий, называются \emph{$''<tex>\alpha$</tex>-эквивалентными} '' и обозначаются $<tex>f \equiv_\alpha g$</tex>.

Функции |<tex>\lambda x -> \to \lambda y -> \to x y z| </tex> и |<tex>\lambda a -> \to \lambda x -> \to a x z| </tex> являются $<tex>\alpha$</tex>-эквивалентными,а |<tex>\lambda x -> \to \lambda y -> \to y z| </tex> и |<tex>\lambda y -> \to \lambda x -> \to y z|~</tex> {{--- }} нет.