Untyped Lambda Calculus

С 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 \) %3 x x
\( m \, n \) %3 a @ m m a--m n n a--n
\( \lambda x. m \) %3 a λ m x a--m n m a--n

Наша функция \( f \) теперь может быть представлена в виде синтаксического дерева:

%3 l1 λ l2 λ l1--l2 xl x l1--xl yl y l2--yl a1 @ l2--a1 x x y y two 2 tree 3 a2 @ a1--a2 a3 @ a1--a3 a4 @ a2--a4 plus plus a2--plus a3--y a6 @ a3--a6 a4--two a5 @ a4--a5 a5--x pow pow a5--pow a6--tree prod prod a6--prod

Кодированием таких деревьев мы и займемся с помощью алгебраических типов:

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{(это неправда!)}‌‌
\]

Для решения проблемы захвата существует несколько решений:

  1. Использовать для связанных и свободных переменных символы из различного алфавита (соглашение Баррендрегта). Идея богатая, но мало реализуемая на практике.
    \[
    (\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‌‌
    \]
  2. Убрать все имена связанных переменных, заменив их номерами, показывающими, сколько лямбд назад они были связаны. Такой способ называется индексами (нотацией) де Брауна и используется в большинстве языков программирования благодаря своей вычислительной эффективности.
    \[
    (\lambda (\lambda \color{green}1\color{black} \, \color{red}2\color{black}) \, \color{red}1 \color{black}) \, \color{blue}x‌‌
    \]
  3. Мы же пойдем третим путем: каждый раз, встречая конфликт при подстановке, мы будем осуществлять переименование связанных переменных в некоторые еще не использованные имена. Это не так эффективно, зато очень похоже на то, что делает человек, оперируя вручную с лямбда-исчислением.

Для начала создадим функцию, которая позволит нам генерировать новое имя, не конфликтующее ни с каким из представленных. Для этого будем передавать множество потенциальных конфликтов в качестве аргумента.

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\). Она проводится следующим образом:

  1. \( (\lambda x.M) \, N = M[x:=N] \), то есть простым \(\beta\)-преобразованием;
  2. \( M \rightarrow_{\beta} N \Rightarrow M \, Z \Rightarrow N \, Z \), то есть редукция в первом терме (алгоритме) применения.
  3. \( M \rightarrow_{\beta} N \Rightarrow Z \, M \Rightarrow Z \, N \), то есть редукция во втором терме (аргументе) применения.
  4. \( 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)
Показать комментарии