С 2015 года я читаю лекции в ИТМО, так или иначе связанные с функциональным программированием. Обычно первые несколько лекций посвещены нетипизированному лямбда-исчислению, его построению и задачам, которые можно на нем решить. Студенты воспринимают такой сугубо теоретический материал с некоторым скрипом, и хорошо проникаются только когда им предлагается написать код лямбда-исчисления самим. В связи с этим кажется было бы интересно попробовать смешать неприятное с бесполезным сделать описание исчисления сразу с реализацией кода. Разумеется, при этом пострадает полнота и глубина материала, но для хорошего теоретического понимания есть Баррендрегт или (скромно) мои лекции. Здесь же мы сконцентрируемся на практическом аспекте.
Начнем, непосредственно, с введения формального языка, который позволит нам описывать термы лямбда-исчисления. Простейшим элементом исчисления являются переменные — элементы множества \(V = {x, y, z, \ldots}\) произвольных символов латинского алфавита. Любая подобная переменная уже будет считаться термом:
\[x
\in V \Rightarrow x \in \Lambda.
\]
Также обязательным условием построения любого исчисления является то, что термом является терм в скобках:
\[
t \in \Lambda \Rightarrow (t) \in \Lambda.
\]
Теперь мы можем строить уже бесконечное множество термов:
\[
x, y, (x), ((x)), (((z))), \ldots
\]
Однако это явно не то, что мы хотим в итоге, ведь наше исчисление должно иметь способность выражать любое вычисление. А значит, требуется добавить в него еще видов формул. Понятная и естественная конструкция — это применение. Терм, представляющий из себя функцию, применяется к некоторому терму (представляющий аргумент), в результате чего получается новый терм. В лямбда-исчислении это можно выразить следующим образом:
\[
m, n \in \Lambda \Rightarrow (m \, n) \in \Lambda,
\]
что позволяет нам писать еще больше бессмысленных конструкций:
\[
(x \, y), ((x \, y) z), ((x \,y) z) (m n), \ldots
\]
Последняя, но очень важная конструкция — абстрация терма по переменной, позволяющая показать зависимость некоторой функции от своего аргумента. По историческим причинам она пишется через букву \( \lambda \), что и дало название исчислению:
\[
x \in V, m \in \Lambda \Rightarrow \lambda x. m \in \Lambda.
\]
Если допустить, что у нас есть некоторые именованные термы (e.g. plus, prod и pow), представляющие те или иные операторы (+, *, ^), мы можем написать произвольную арифметическую функцию:
\[
f(x,y) = x^2 + 3 \cdot y \rightarrow \lambda x.\lambda y.((plus ((pow \, x) 2)) ((prod \, 3) y))
\]
Из-за обилия скобочек выражение выглядит совершенно нечитаемым, так что для начала добавим несколько соглашений, которые позволят упростить запись. В первую очередь, это правила ассоциативности. Применение мы будем считать ассоциативным влево, а абстракцию вправо:
\[
(m n) (k) = m \, n \, k \\
\lambda x. \lambda y. m = \lambda x \, y. m
\]
Теперь переписать ту же конструкцию можно короче и совсем понятно:
\[
f(x,y) = x^2 + 3 \cdot y \rightarrow \lambda x \, y. plus \, (pow \, x \, 2) (prod \, 3 \, y)
\]
Чтоб еще сильнее забыть про скобки, начнем думать про наши термы не как про строки, а как про синтаксические деревья. Правила переходов в деревья будут следующие:
| Терм | Дерево |
|---|---|
| \( x \) | |
| \( m \, n \) | |
| \( \lambda x. m \) |
Наша функция \( f \) теперь может быть представлена в виде синтаксического дерева:
Кодированием таких деревьев мы и займемся с помощью алгебраических типов:
import Data.Text (Text)
data Term = Var Text -- переменные
| App Term Term -- аппликация
| Lam Text Term -- абстракция
deriving (Show)
Чтоб сконструировать интересующий нас терм \( f \) нам также потребуется поддержка числовых литералов (числа 2 и 3). Их можно добавить в наше исчисление (добавив еще один конструктор, например, Lit Int) или сэмулировать через переменные two и tree:
{-# LANGUAGE OverloadedStrings #-}
f :: Term
f = Lam "x" (Lam "y" (App (App (Var "plus") xSqr) p3y))
where xSqr = App (App (Var "pow") (Var "x")) (Var "two")
p3y = App (App (Var "prod") (Var "tree")) (Var "y")
Полученное выражение вновь изобилует скобками и вообще трудно перевариваемо:
Вывод термов
Чтоб как-то жить с этим, лучше сразу написать некоторый pretty printer, который будет выводить наши термы красиво. Начнем с простой реализации, печатающей все скобки:
import Data.Monoid ((<>))
pretty :: Term -> Text
pretty (Var name) = name
pretty (App algo arg) = "(" <> pretty algo <> " " <> pretty arg <> ")"
pretty (Lam var body) = "λ" <> var <> "." <> pretty body
Читать подобный вывод уже можно, но все же лишние скобки явно затрудняют понимание:
ghci> import Data.Text.IO as TIO
ghci> TIO.putStrLn (pretty f)
λx.λy.((plus ((pow x) two)) ((prod tree) y))
Скобки требуется убирать вокруг аппликации в трех случаях: если она верхнеуровневая, если она является алгоритмом (algo) другой аппликации или если она является телом (body) абстракции. Модифицируем соответствующим образом нашу функцию:
data Parens = ParensLess | ParensFull
pretty :: Term -> Text
pretty = pretty' ParensLess
where
pretty' :: Parens -> Term -> Text
pretty' _ (Var name) = name
pretty' ParensLess (App algo arg) = pretty' ParensLess algo <> " " <> pretty' ParensFull arg
pretty' ParensFull app@(App _ _) = "(" <> pretty' ParensLess app <> ")"
pretty' _ (Lam var body) = "λ" <> var <> "." <> pretty' ParensLess body
Теперь мы получаем красивый и наглядный вывод:
ghci> import Data.Text.IO as TIO
ghci> TIO.putStrLn (pretty f)
λx.λy.plus (pow x two) (prod tree y)
Последним штрихом будет сжатие вложенных лямбд в одну, это нужно делать если текущая лямбда находится в теле другой лямбды. Общая логика: если лямбда в теле другой лямбды, то добавляем переменную в список переменных, если вложение лямбд кончилось, то ставим точку и описываем тело. Реализация такова:
data Position = AppAlgo | AppArg | LamBody | Other
pretty :: Term -> Text
pretty = pretty' Other
where
prettyLB :: Term -> Text
prettyLB (Lam var body) = var <> pretty' LamBody body
prettyLB _ = undefined
pretty' :: Position -> Term -> Text
pretty' LamBody lam@(Lam _ _) = " " <> prettyLB lam
pretty' AppAlgo lam@(Lam _ _) = "(" <> pretty' Other lam <> ")"
pretty' _ lam@(Lam _ _) = "λ" <> prettyLB lam
pretty' LamBody term = "." <> pretty' Other term
pretty' _ (Var name) = name
pretty' AppArg app@(App _ _) = "(" <> pretty' Other app <> ")"
pretty' _ (App algo arg) = pretty' AppAlgo algo <> " " <> pretty' AppArg arg
И финальный вывод:
ghci> import Data.Text.IO as TIO
ghci> TIO.putStrLn (pretty f)
λx y.plus (pow x two) (prod tree y)
Ввод термов
Помимо красивого вывода нам потребуется как-то забивать термы в наш калькулятор, поскольку набирать что-то вроде Lam "x" (Lam "y" (App (... совсем не весело. Для этого нам потребуется реализовать парсер для лямбда-термов. В идеале мы должны получить функцию, способную распарсить любой наш сжатый вывод функции pretty, то есть обеспечивающую следующее правило:
\[
parse \circ pretty = id
\]
Конечно, на самом деле мы должны обрабатывать ошибки синтаксиса и все такое, а потому наша функция parse будет несколько сложнее. Сама стратегия парсинга будет следующая: любой терм мы будем рассматривать как потенциальную аппликацию, т.е. несколько термов идущих друг за другом. Потенциальной она является в том смысле, что терм может оказаться всего один, и тогда никакой аппликации он не будет. Такой терм, не являющийся аппликацией, мы будем называть натуральным термом:
\[
\begin{align*}
term &::= {natural \, term}^n \\
natural \, term &::= (term) | variable | abstraction
\end{align*}
\]
Начнем нашу имплементацию с подключения необходимых модулей парсинга (здесь использован мой любимый attoparsec, для классического parsec или модного, но медленного megaparsec все аналогично), а также написания нескольких вспомогательных функций.
import Control.Applicative ((<$>), (<*>), (<|>))
import Control.Monad (void)
import Data.Text (Text, pack)
import Data.Attoparsec.Text
-- Один или несколько пробелов подряд
spaces :: Parser ()
spaces = void $ many' space
-- Парсит выражение, со всеми пробелами после него, пробелы опускает.
spaced :: Parser a -> Parser a
spaced x = x <* spaces
-- Парсит одну точку и опускает вывод парсера.
dot :: Parser ()
dot = void $ spaced (char '.')
-- Парсит символ лямбды или \\ или L и опускает вывод парсера.
lambda :: Parser ()
lambda = void $ spaced (char '\\' <|> char 'λ' <|> char 'L')
-- Парсит выражение окруженное скобками; перед открывающей и
-- после закрываающей скобок могут идти пробелы, которые будут съедены.
parens :: Parser a -> Parser a
parens x = spaced (char '(') *> x <* spaced (char ')')
-- Парсит строку, начинающуюся с символов латинского алфавита и
-- содержащую латинские символы, цифры и символ '.
name :: Parser Text
name = (pack .) . (:) <$> oneOf ['a'..'z'] <*> many' (letter <|> digit <|> char '\'')
where
oneOf = choice . (char <$>)
Теперь можно реализовать функции, которые будут прочитывать терм и натуральный терм в формулировках, данных выше:
-- Прочитывает не менее одного натурального терма; в случае
-- если их больше одной, соединяет их в один с помощью аппликации
-- по правилам левой ассоциативности.
term :: Parser Term
term = foldl1 App <$> many1 (spaced naturalTerm)
-- Прочитывает терм, возможно содержащий аппликацию, в скобках,
-- либо переменную, либо лямбда-абстракцию.
naturalTerm :: Parser Term
naturalTerm = parens term <|> variable <|> abstraction
Осталось написать всего два парсера: для переменных и абстракции. Их вид столь же тривиален, что и у парсеров выше:
-- Парсит одну переменную.
variable :: Parser Term
variable = Var <$> name
-- Парсит лямбда-абстракцию, как символ лямбды, не менее 1 переменной,
-- точку и терм, являющийся телом абстракции; сворачивает переменные
-- во вложенные лямбда-абстракции по правилу правой ассоциативности.
abstraction :: Parser Term
abstraction = do lambda
vars <- many1 (spaced name)
dot
expr <- term
pure $ foldr Lam expr vars
Протестировать наши парсеры можно с помощью такой функции:
parseTerm :: Text -> Either String Term
parseTerm = parseOnly term
В интерпретаторе проверим, что все читается верно:
ghci> :set -XOverloadedStrings
ghci> Right t = parseTerm "λx y.plus (pow x two) (prod tree y)"
ghci> t
Lam "x" (Lam "y" (App (App (Var "plus") (App (App (Var "pow") (Var "x")) (Var "two"))) (App (App (Var "prod") (Var "tree")) (Var "y"))))
ghci> pretty t
λx y.plus (pow x two) (prod tree y)
Наполнение смыслом
Теперь пришло время наполнить наше исчисление смыслом. Для этого требуется ввести несколько правилм переписывания одних термов в другие, которые мы и будем считать вычислениями.
Прежде чем начать, введем пару определений. В зависимости от присутствия или отсутствия переменной под символом лямбды в абстракции мы будем делить все переменные на свободные и связанные. Начнем с интутитивного примера:
\[
(\lambda \color{red}x \color{black}. (\lambda \color{green}x \color{black}. \color{green}x \color{black} \, y) \, \color{red}x \color{black}) \, \color{blue}x
\]
Иксы разного цвета как бы "связываются" разными лямбдами. Проследить интуитивно это можно следующим образом, снимая некоторую лямбду можно "освободить" ту или иную переменную, поскольку её имя больше не будет означать, что она является аргументом какой-либо функции. После столь водянистого пояснения дадим нормальное определение:Для произвольного терма \( t \) множеством его свободных переменных \( FV(t) \) называют множество, сконструированное по следующим правилам (далее подразумевается, что \( x \in V, \, M, N \in \Lambda \)):
\[
\begin{align*}
FV(x) &= \{x\} \\
FV(M \, N) &= FV(M) \cup FV(N) \\
FV(\lambda x. M) &= FM(M) \backslash \{x\}
\end{align*}
\]
Аналогично задается множество \( BV(t) \) связанных переменных:
\[
\begin{align*}
BV(x) &= \varnothing \\
BV(M \, N) &= FV(M) \cup FV(N) \\
BV(\lambda x. M) &= BV(M) \cup \{x\}
\end{align*}
\]
Соответствующие функции на Haskell будут в точности повторять определение:
import Data.Set (Set, delete, empty,
insert, singleton, union)
free :: Term -> Set Name
free (Var var) = singleton var
free (App algo arg) = free algo `union` free arg
free (Lam var body) = var `delete` free body
bound :: Term -> Set Name
bound (Var var) = empty
bound (App algo arg) = bound algo `union` bound arg
bound (Lam var body) = var `insert` free body
В лямбда-исчислении существует единственная нетривиальная аксиома — два терма являются равными, если они равны с точностью до переименования связанных переменных. Таким образом, следующие термы равны:
\[
\lambda \color{red}x \color{black} \, \color{green}y \color{black} . \color{red} x \color{black} = \lambda \color{red}z \color{black} \, \color{green}w \color{black} . \color{red} z \color{black} = \lambda \color{red}y \color{black} \, \color{green}x \color{black} . \color{red} y \color{black}
\]
Реализуем это, сделав наши термы представителем классов типов Eq следующим образом:
instance Eq Term where
Var a == Var b = a == b
App a b == App a' b' = a == a' && b == b'
Lam v b == Lam v' b' = b == substitute b' v' (Var v)
_ == _ = False
Здесь нам требуется реализовать дополнительную функцию подставновки, которая бы позволила заменять имена переменных. На самом деле мы реализуем гораздо более сильную версию подстановки, позволяющую подставлять вместо всех свободных вхождений переменной произвольный терм. Для этого в лямбда-исчислении есть принятое формальное определение подстановки.
Подстановкой \( M[x:=N] \) терма \( N \) вместо всех свободных вхождений переменной \( x \) в терм \( M \) называют терм, образованный по следующим правилам (как обычно, \( x \in V, \, M, N, P, Q \in \Lambda \)):
\[
\begin{align*}
x[x:=N] &= N \\
y[x:=N] &= y \\
(P \, Q)[x:=N] &= (P[x:=N]) \, (Q[x:=N]) \\
(\lambda x. M)[x:=N] &= \lambda x. M \\
(\lambda y. M)[x:=N] &= \lambda y. (M[x:=N]), \text{ если } x \not\in FV(N)
\end{align*}
\]
В последнем пункте есть дополнительное условие. Если его не соблюдать, то некоторые подставновки будут приводить к неприятным последствиям, а именно изменению структуры терма, называемой захватом переменной:
\[
(\lambda x.y)[y:=x] = \lambda x.x \, \color{red}\text{(это неправда!)}
\]
Для решения проблемы захвата существует несколько решений:
- Использовать для связанных и свободных переменных символы из различного алфавита (соглашение Баррендрегта). Идея богатая, но мало реализуемая на практике.
\[
(\lambda \color{red}x' \color{black}. (\lambda \color{green}y' \color{black}. \color{green}y' \color{black} \, \color{red}x' \color{black}) \, \color{red}x' \color{black}) \, \color{blue}x
\] - Убрать все имена связанных переменных, заменив их номерами, показывающими, сколько лямбд назад они были связаны. Такой способ называется индексами (нотацией) де Брауна и используется в большинстве языков программирования благодаря своей вычислительной эффективности.
\[
(\lambda (\lambda \color{green}1\color{black} \, \color{red}2\color{black}) \, \color{red}1 \color{black}) \, \color{blue}x
\] - Мы же пойдем третим путем: каждый раз, встречая конфликт при подстановке, мы будем осуществлять переименование связанных переменных в некоторые еще не использованные имена. Это не так эффективно, зато очень похоже на то, что делает человек, оперируя вручную с лямбда-исчислением.
Для начала создадим функцию, которая позволит нам генерировать новое имя, не конфликтующее ни с каким из представленных. Для этого будем передавать множество потенциальных конфликтов в качестве аргумента.
import Data.Text (Text, pack)
import Data.Set (Set, member)
-- Генерируем бесконечный список предлагаемых имен и берем первое,
-- которое пока не встретилось в списке.
fresh :: Set Text -> Text
fresh conflicts = head . dropWhile (`member` conflicts) $ names
where
-- Простые имена — это просто малые буквы латинского алфавита
primitiveNames = map (:[]) letters
-- Составные имена состоят из буквы и цифры
complexNames = [(l:n) | n <- numbers, l <- letters]
-- Полный список имен
names = map pack $ primitiveNames ++ complexNames
-- Используемые буквы и числа
letters = ['a' .. 'z']
numbers = map show [1..]
Используя эту функцию, можно сделать еще одну, заменяющую все имена связанных переменных так, чтоб они не входили в список конфликтных имен. Такое преобразование имен связанных переменных никак не меняет сам терм и называется \(\alpha\)-преобразованием:
alpha :: Set Text -> Term -> Term
alpha conflicts var@(Var _) = var
alpha conflicts (App algo arg) = App (alpha conflicts algo) (alpha conflicts arg)
alpha conflicts (Lam var body) = if hasConflict then renamed_lam else alpha_lam
where
hasConflict = var `member` conflicts
alpha_lam = Lam var (alpha conflicts body)
renamed_lam = Lam new_var new_body
new_var = fresh $ conflicts `union` free body
new_body = substitute body var (Var new_var)
Для написания этой функции нам вновь пришлось прибегнуть к функции substitute, поскольку при смене переменной под лямбдой нам потребуется заменить все её упоминание в теле абстрации. Теперь у нас есть все, чтоб реализовать эту волшебную функцию:
substitute :: Term -> Text -> Term -> Term
substitute var@(Var var') name expr = if var' == name then expr else var
substitute (App algo arg) name expr = App (substitute algo name expr) (substitute arg name expr)
substitute lam@(Lam var body) name expr = if var == name then lam else new_lam
where
alpha_lam = alpha (free expr) lam
new_body = substitute body name expr
new_lam = if var `member` free expr then substitute alpha_lam name expr
else Lam var new_body
Редукция
В лямбда-вычислении мы допускаем два вида редукции — одностороннего преобразования или "упрощения", которое и будет представлять вычисление. Первый такой вид редукции тривиален и называется \(\eta\)-преобразованием:
\[
\lambda x. M \, x = M
\]
Оно выводится из тривиальных соображений, о чем можно почитать у того же Баррендрегта. Реализуется оно практически столь же просто:
eta :: Term -> Term
eta (Lam var body) = case body of
App algo (Var v)
| var == v && v `notMember` free algo = algo
_ = Lam var (eta body)
eta (App algo arg) = App (eta algo) (eta arg)
eta var = var
Главное же преобразование — это единственное правило вывода в лямбда-исчислении — \(\beta\)-преобразование:
\[
(\lambda x.M) \, N = M[x:=N]
\]
То есть любое применение лямбда-абстракции к какому-либо терму выполняется путем замены переменной абстракции (аргумента) на конкретное значение. На базе такого преобразования возможно написать правила одношаговой \(\beta\)-редукции \( M \rightarrow_{\beta} N\). Она проводится следующим образом:
- \( (\lambda x.M) \, N = M[x:=N] \), то есть простым \(\beta\)-преобразованием;
- \( M \rightarrow_{\beta} N \Rightarrow M \, Z \Rightarrow N \, Z \), то есть редукция в первом терме (алгоритме) применения.
- \( M \rightarrow_{\beta} N \Rightarrow Z \, M \Rightarrow Z \, N \), то есть редукция во втором терме (аргументе) применения.
- \( M \rightarrow_{\beta} N \Rightarrow \lambda x. M \Rightarrow \lambda x. N \), то есть редукция в теле абстракции.
Релизуем это следующим образом:
beta :: Term -> Term
beta var@(Var _) = var
beta (Lam var body) = Lam var (beta body)
beta (App algo arg) = case algo of
Lam var body -> substitute body var arg
_ -> if algo /= algo' then App algo' arg
else App algo arg'
where
algo' = beta algo
arg' = beta arg
На этом все! У нас получился полный лямбда-калькулятор с парсером, красивым выводом и разными видами редукции. Превращать любой терм в нормальную форму, при её наличии, можно подобной простой функцией:
reduce :: Term -> Term
reduce term | beta term == term = eta term
| otherwise = reduce (beta term)
Ну, а попрактиковаться в применении лямбда-исчисления можно, например, на кодировании натуральных и целых чисел, как это описано в Википедии.
Я же напоследок приведу полный листинг получившегося:
module UntypedLambda where
import Control.Applicative ((<$>), (<*>), (<|>))
import Control.Monad (void)
import Data.Text (Text, pack)
import Data.Attoparsec.Text
import Data.Set (Set, delete, empty,
insert, singleton, union,
member, notMember)
data Term = Var Text -- переменные
| App Term Term -- аппликация
| Lam Text Term -- абстракция
deriving (Show)
-- Pretty Print
data Position = AppAlgo | AppArg | LamBody | Other
pretty :: Term -> Text
pretty = pretty' Other
where
prettyLB :: Term -> Text
prettyLB (Lam var body) = var <> pretty' LamBody body
prettyLB _ = undefined
pretty' :: Position -> Term -> Text
pretty' LamBody lam@(Lam _ _) = " " <> prettyLB lam
pretty' AppAlgo lam@(Lam _ _) = "(" <> pretty' Other lam <> ")"
pretty' _ lam@(Lam _ _) = "λ" <> prettyLB lam
pretty' LamBody term = "." <> pretty' Other term
pretty' _ (Var name) = name
pretty' AppArg app@(App _ _) = "(" <> pretty' Other app <> ")"
pretty' _ (App algo arg) = pretty' AppAlgo algo <> " " <> pretty' AppArg arg
-- Parsing
spaces :: Parser ()
spaces = void $ many' space
-- Парсит выражение, со всеми пробелами после него, пробелы опускает.
spaced :: Parser a -> Parser a
spaced x = x <* spaces
-- Парсит одну точку и опускает вывод парсера.
dot :: Parser ()
dot = void $ spaced (char '.')
-- Парсит символ лямбды или \\ или L и опускает вывод парсера.
lambda :: Parser ()
lambda = void $ spaced (char '\\' <|> char 'λ' <|> char 'L')
-- Парсит выражение окруженное скобками; перед открывающей и
-- после закрываающей скобок могут идти пробелы, которые будут съедены.
parens :: Parser a -> Parser a
parens x = spaced (char '(') *> x <* spaced (char ')')
-- Парсит строку, начинающуюся с символов латинского алфавита и
-- содержащую латинские символы, цифры и символ '.
name :: Parser Text
name = (pack .) . (:) <$> oneOf ['a'..'z'] <*> many' (letter <|> digit <|> char '\'')
where
oneOf = choice . (char <$>)
-- Прочитывает не менее одного натурального терма; в случае
-- если их больше одной, соединяет их в один с помощью аппликации
-- по правилам левой ассоциативности.
term :: Parser Term
term = foldl1 App <$> many1 (spaced naturalTerm)
-- Прочитывает терм, возможно содержащий аппликацию, в скобках,
-- либо переменную, либо лямбда-абстракцию.
naturalTerm :: Parser Term
naturalTerm = parens term <|> variable <|> abstraction
-- Парсит одну переменную.
variable :: Parser Term
variable = Var <$> name
-- Парсит лямбда-абстракцию, как символ лямбды, не менее 1 переменной,
-- точку и терм, являющийся телом абстракции; сворачивает переменные
-- во вложенные лямбда-абстракции по правилу правой ассоциативности.
abstraction :: Parser Term
abstraction = do lambda
vars <- many1 (spaced name)
dot
expr <- term
pure $ foldr Lam expr vars
parseTerm :: Text -> Either String Term
parseTerm = parseOnly term
-- Logic
free :: Term -> Set Text
free (Var var) = singleton var
free (App algo arg) = free algo `union` free arg
free (Lam var body) = var `delete` free body
bound :: Term -> Set Text
bound (Var var) = empty
bound (App algo arg) = bound algo `union` bound arg
bound (Lam var body) = var `insert` free body
instance Eq Term where
Var a == Var b = a == b
App a b == App a' b' = a == a' && b == b'
Lam v b == Lam v' b' = b == substitute b' v' (Var v)
_ == _ = False
-- Генерируем бесконечный список предлагаемых имен и берем первое,
-- которое пока не встретилось в списке.
fresh :: Set Text -> Text
fresh conflicts = head . dropWhile (`member` conflicts) $ names
where
-- Простые имена — это просто малые буквы латинского алфавита
primitiveNames = map (:[]) letters
-- Составные имена состоят из буквы и цифры
complexNames = [(l:n) | n <- numbers, l <- letters]
-- Полный список имен
names = map pack $ primitiveNames ++ complexNames
-- Используемые буквы и числа
letters = ['a' .. 'z']
numbers = map show [1..]
alpha :: Set Text -> Term -> Term
alpha conflicts var@(Var _) = var
alpha conflicts (App algo arg) = App (alpha conflicts algo) (alpha conflicts arg)
alpha conflicts (Lam var body) = if hasConflict then renamed_lam else alpha_lam
where
hasConflict = var `member` conflicts
alpha_lam = Lam var (alpha conflicts body)
renamed_lam = Lam new_var new_body
new_var = fresh $ conflicts `union` free body
new_body = substitute body var (Var new_var)
substitute :: Term -> Text -> Term -> Term
substitute var@(Var var') name expr = if var' == name then expr else var
substitute (App algo arg) name expr = App (substitute algo name expr) (substitute arg name expr)
substitute lam@(Lam var body) name expr = if var == name then lam else new_lam
where
alpha_lam = alpha (free expr) lam
new_body = substitute body name expr
new_lam = if var `member` free expr then substitute alpha_lam name expr
else Lam var new_body
-- Evaluation
eta :: Term -> Term
eta (Lam var body) = case body of
App algo (Var v)
| var == v && (v `notMember` free algo) -> algo
_ -> Lam var (eta body)
eta (App algo arg) = App (eta algo) (eta arg)
eta var = var
beta :: Term -> Term
beta var@(Var _) = var
beta (Lam var body) = Lam var (beta body)
beta (App algo arg) = case algo of
Lam var body -> substitute body var arg
_ -> if algo /= algo' then App algo' arg
else App algo arg'
where
algo' = beta algo
arg' = beta arg
reduce :: Term -> Term
reduce term | beta term == term = eta term
| otherwise = reduce (beta term)