Эта статья будет публичной, но в статусе DRAFT, скорее всего я буду ее дополнять и пересматривать, пока тут какие-то базовые определения и доказательство того, что у (λx.xx)(λx.xx) нет нормальной формы. Скорее всего тут есть некоторые неточности и даже ошибки, буду исправлять в процессе.

#agda #lambdacalculus

Определим модуль и импортируем необходимые модули

module LambdaCalc where

open import Data.Nat
open import Data.Bool hiding (_≟_)
import Relation.Binary.PropositionalEquality as Eq
open Eq hiding (subst)
open Eq.≡-Reasoning
open import Relation.Nullary.Decidable 
open import Data.Empty using (⊥; ⊥-elim) 
open import Data.Unit using (⊤; tt) 
open import Data.Product

Начнем с определения термов лямбда-исчисления. Для простоты будем использовать индексы де Брауна для переменных, это когда переменные не именуются, а нумеруются (индексируются), индекс показывает, сколько лямбд назад переменная была связана:

λx. (λy. x y) ↔ λ (λ 1 0) λx. x (λy. x y y) ↔ λ 0 (λ 1 0 0)

-- Определение термов лямбда-исчисления
data Λ : Set where     
  _`  : ℕ → Λ          -- Переменная
  λ'_  : Λ → Λ         -- Лямбда-абстракция 
  _∘_  : Λ → Λ → Λ     -- Применение 

Подстановка нужна для реализации бета-редукции:

-- Подстановка терма вместо переменной
subst : Λ → ℕ → Λ → Λ 
--Если переменная равна той же вместо которой мы подставляем, то подставляем, иначе не подставляем
--Как работают ⌊_⌋ и ≟ надо будет как-нибудь объяснить, но пока поверьте, что это такое хитрое сравнение на равенство
subst (x `) y s = if ⌊ x ≟ y ⌋ then s else (x `)
--Внутрь лямбда абстрации тоже можем подставить(увеличиваем на единицу значение искомого индекса т.к. погружаемся глубже)
subst (λ' t) y s = λ' (subst t (suc y) s)
--Можем подставить с обеих сторон применения
subst (t ∘ u) y s = (subst t y s) ∘ (subst u y s)

Теперь определим одношаговую бета-редукцию:

-- Одношаговая бета-редукция
data _→β_ : Λ → Λ → Set where
  --Если есть абстракция и применение, то можем применить подстановку
  beta : ∀ {t u} → ((λ' t) ∘ u) →β (subst t 0 u)
  --Можно редуцировать левую часть применения
  app₁ : ∀ {t t' u} → t →β t' → (t ∘ u) →β (t' ∘ u)
  --Можно редуцировать правую часть применения
  app₂ : ∀ {t u u'} → u →β u' → (t ∘ u) →β (t ∘ u')
  --Можно редуцировать под лямбда абстракцией
  lam  : ∀ {t t'} → t →β t' → (λ' t) →β (λ' t')

Определяем многошаговую редукцию:

-- Многошаговая редукция (→β*)
data _→β*_ : Λ → Λ → Set where
  refl : ∀ {M} → M →β* M
  step : ∀ {M N P} → M →β N → N →β* P → M →β* P

Определяем нормальную форму:

Normal : Λ → Set
--Переменная уже в нормальной форме
Normal (x `)    = ⊤
--Если есть лямбда абстракция и применение к ней, то это редекс т.е. можно использовать подстановку
Normal ((λ' _) ∘ _) = ⊥
--Применение имеет нормальную форму, если оба аргумента имеют нормальную форму
Normal (M ∘ N)  = Normal M × Normal N
--Лямбда абстракция имеет нормальную форму, если терм внутри имеет нормальную форму
Normal (λ' M)    = Normal M

-- Определение Ω = (λx.xx)(λx.xx)
Ω : Λ
Ω = (λ' ((0 `) ∘ (0 `))) ∘ (λ' ((0 `) ∘ (0 `)))

--xx не редуцируется
l1 : ∀ {x t} → ((x `) ∘ (x `)) →β t → ⊥ 
l1 (app₁ ())  --интересно, кстати, почему этого кейса достаточно и Agda не требует еще разобрать app₂
--() это так называемый absurd pattern, т.е. не существует такой β-редукции, которую мы могли бы применить к левой части применения

--λx.xx не редуцируется 
l2 : ∀ {x t} → (λ' ((x `) ∘ (x `))) →β t → ⊥ 
l2 (lam b) = l1 b

--(λx.xx)(λx.xx) редуцируется в себя
l3 : Ω →β Ω 
l3 = beta

--Ω всегда редуцируется в Ω
Ω→βΩ : ∀ T → Ω →β T → T ≡ Ω
--Если использовать применение, то Ω переходит в себя по определению
Ω→βΩ t beta = refl
--Если мы редуцировали левую часть применения, то это могла быть только λx.xx, что невозможно
Ω→βΩ _ (app₁ b) = ⊥-elim (l2 b)
-- А вот тут почему-то требует app₂ проверить :) 
Ω→βΩ _ (app₂ b) = ⊥-elim (l2 b)

Ну и собственно доказываем, что у Ω нет нормальной формы

--У Ω нет нормальной формы
no-normal-form : ∀ {N} → Ω →β* N → Normal N → ⊥ 
--Тут это другой refl из многошаговой β-редукции
no-normal-form refl ()
--Если это была редукция, то Ω перешла в себя
no-normal-form (step beta steps) nf = no-normal-form steps nf
--Остальные варианты невозможны
no-normal-form (step (app₁ t) steps) nf = l2 t
no-normal-form (step (app₂ t) steps) nf = l2 t

Используемые символы и их коды:

Символ	Код
→	\to
Λ	\Lambda
λ	\lambda
⊤	\top
⊥	\bot
ℕ	\bN
∘	\o
∀	\forall
⌊	\clL
⌋	\clR
≟	\?=
₁	_1
₂	_2
β	\beta
Ω	\Omega