ULCOmega.agda

{-# OPTIONS --safe #-}

module ULCOmega where

open import Data.Nat.Base using (ℕ ; zero ; suc)
open import Data.Fin.Base as Fin using (Fin)

import Data.Nat.Literals
import Data.Fin.Literals
open import Data.Unit using (⊤ ; tt) -- for instance resolution
open import Agda.Builtin.FromNat

private
  instance
    NumNumber : Number ℕ
    NumNumber = Data.Nat.Literals.number

    FinNumber : ∀ {m} → Number (Fin m)
    FinNumber {m} = Data.Fin.Literals.number m

infix 10 `_
infixl 5 _·_
infix 3 ƛ_
infix 2 _≡β_
infix 2 _⟶_

data Term : ℕ → Set where
  `_ : ∀ {n} → Fin n → Term n
  ƛ_ : ∀ {n} → Term (suc n) → Term n
  _·_ : ∀ {n} → Term n → Term n → Term n

data Val : Term 0 → Set where
  ƛ/v_ : (e : Term 1) → Val (ƛ e)

-- extending the de Bruijn index: skip the outermost variable
i-ext : ∀ {n m} → (Fin n → Fin m) → (Fin (suc n) → Fin (suc m))
i-ext ren Fin.zero      = Fin.zero
i-ext ren (Fin.suc idx) = Fin.suc (ren idx)

t-rename : ∀ {n m} → Term n → (Fin n → Fin m) → Term m
t-rename (` x)     ren = ` ren x
t-rename (ƛ e)     ren = ƛ (t-rename e (i-ext ren))
t-rename (e₁ · e₂) ren = t-rename e₁ ren · t-rename e₂ ren

-- extending the substitution: skip the outermost variable
t-ext : ∀ {n m} → (Fin n → Term m) → (Fin (suc n) → Term (suc m))
t-ext ϑ Fin.zero      = ` Fin.zero
t-ext ϑ (Fin.suc idx) = t-rename (ϑ idx) Fin.suc

t-subst : ∀ {n m} → Term n → (Fin n → Term m) → Term m
t-subst (` x)     ϑ = ϑ x
t-subst (ƛ e)     ϑ = ƛ (t-subst e (t-ext ϑ))
t-subst (e₁ · e₂) ϑ = t-subst e₁ ϑ · t-subst e₂ ϑ

------------------------------------------------------------

0-maps-to : ∀ {n} → Term n → Fin (suc n) → Term n
0-maps-to e Fin.zero      = e
0-maps-to e (Fin.suc idx) = ` idx

-- with K for lam, app, etc
data _≡β_  : ∀ {n} → (e e′ : Term n) → Set where
  E-refl : ∀ {n} {e : Term n} → e ≡β e
  E-sym : ∀ {n} {e e′ : Term n} →
      e′ ≡β e  →
    -----------
      e ≡β e′

  E-trans : ∀ {n} {e e′ e″ : Term n} →
      e ≡β e″  →
      e″ ≡β e′ →
    -----------
      e ≡β e′

  E-β : ∀ {n} {e : Term (suc n)} {e′ : Term n} →
      ((ƛ e) · e′) ≡β t-subst e (0-maps-to e′)

  E-ƛ : ∀ {n} {e e′ : Term (suc n)} →
          e ≡β e′      →
    --------------------
      (ƛ e) ≡β (ƛ e′)

  E-AppL : ∀ {n} {e₁ e₁′ : Term n} →
          (e₂ : Term n) →
            e₁ ≡β e₁′   →
    --------------------------
      (e₁ · e₂) ≡β (e₁′ · e₂)

  E-AppR : ∀ {n} {e₂ e₂′ : Term n} →
          (e₁ : Term n) →
            e₂ ≡β e₂′ →
    --------------------------
      (e₁ · e₂) ≡β (e₁ · e₂′)

ω³ : Term 0
ω³ = ƛ (` 0 · ` 0 · ` 0)

inf3 : ω³ · ω³ ≡β (ω³ · ω³ · ω³) · ω³
inf3 =
  E-trans
    E-β
    (E-AppL ω³ E-β)

------------------------------------------------------------

singleton : ∀ {n} → Term n → Fin 1 → Term n
singleton e Fin.zero = e

data _⟶_ : Term 0 → Term 0 → Set where
  R-βv : ∀ {e v} →
    Val v →
    (ƛ e) · v ⟶ t-subst e (singleton v)

  R-AppL : ∀ {e₁ e₁′ e₂} →
          e₁ ⟶ e₁′      →
    ---------------------
     e₁ · e₂ ⟶ e₁′ · e₂

  R-AppR : ∀ {v e e′} →
          Val v       →
          e ⟶ e′     →
    ------------------
      v · e ⟶ v · e′

Ω : Term 0
Ω = (ƛ (` 0 · ` 0)) · (ƛ (` 0 · ` 0))

Ωinf : Ω ⟶ Ω
Ωinf = R-βv (ƛ/v (` 0 · ` 0))