module Просто_типизированное_лямбда_исчисление where

{- Часть 2 | Просто типизированное лямбда исчисление -}

open import Вспомогательные_определения


{-
Определение 2.1. Множество простых типов Π задается индуктивно.
                 Пусть V - некоторое бесконечное множество переменных
                 (в нашем случае множество строк String).
                 ∙ Всякая переменная является типом
                 ∙ Если σ, τ - типы, то σ ⇒ τ - тип
-}

infixr  _⇒_

data Π : Множество where
  тпер : Строка → Π
  _⇒_ : Π → Π → Π

{-
Определение 2.2. Множество безтиповых лямбда-термов Λ задается по индукции.
                 ∙ Все переменные x ∈ V - термы
                 ∙ Если M, N - термы, то их применение (M N) - терм
                 ∙ Если x - переменная, M - терм, то абстракция λx.M - терм
-}

data Λ : Множество where
  λпер : Строка → Λ
  _$_ : Λ → Λ → Λ
  ƛ_!_ : Строка → Λ → Λ

{-
Определение 2.3. Множество связок - V × Π.
                 Элемент этого множества обозначается x : τ
-}

{- Примечание. Чтобы избежать конфликта имен назовем x : τ как x of τ -}

infixl  _типа_

data Связка : Множество where
  _типа_ : Строка → Π → Связка

{-

Определение 2.4. Контекст - список связок. Обозначается Γ, Δ, .. .

Определение 2.5. Область определения (domain) контекста Γ -
                 список [x | (x ∶ _) ∈ Γ ] переменных, входящих в этот контекст.

Определение 2.6. Область значения (range) контекста Γ -
                 список [τ | (_ ∶ τ) ∈ Γ ] типов, входящих в этот контекст.

-}

λКонтекст = Список Связка

область_определения : λКонтекст → Список Строка
область_определения Γ = отобразить (λ { (x типа _) → x}) на Γ

область_значения : λКонтекст → Список Π
область_значения Γ = отобразить (λ { (_ типа τ) → τ}) на Γ

{-
Определение 2.7. Отношение типизации ‌⊢ ⊆ L(Binding) × Λ × Π
                 задется индуктивно правилами вывода.
-}

infixr  ƛ_!_
infixl  _$_
infix  _⊢_∶_
infix  Применить_к_

data _⊢_∶_ : λКонтекст → Λ → Π → Set where
  Аксиома : ∀ {Γ x τ} → x типа τ ∷ Γ ⊢ λпер x ∶ τ
  Абстрагировать : ∀ {Γ x τ M σ} → x типа σ ∷ Γ ⊢ M ∶ τ → Γ ⊢ ƛ x ! M ∶ σ ⇒ τ
  Применить_к_ : ∀ {Γ τ M σ N} → Γ ⊢ M ∶ σ ⇒ τ → Γ ⊢ N ∶ σ → Γ ⊢ (M $ N) ∶ τ

{- Комментарий. Сравните определения 1.1 и 2.1, 1.2 и 2.4, 1.4 и 2.7. -}