Skip to content

Instantly share code, notes, and snippets.

@cheery

cheery/newtry6.agda

Created January 26, 2023 16:29
Show Gist options
  • Save cheery/eaf5630c193488c088669b24559a1c63 to your computer and use it in GitHub Desktop.
Save cheery/eaf5630c193488c088669b24559a1c63 to your computer and use it in GitHub Desktop.
Download ZIP
Normalizer for lambda calculus
Raw
newtry6.agda
module newtry6 where
-- derived from https://gist.github.com/rntz/2543cf9ef5ee4e3d990ce3485a0186e2
-- http://eprints.nottingham.ac.uk/41385/1/th.pdf
open import Level
open import Function using (id; _∘_)
infixr 5 _⇒_
data Ty : Set where
base : Ty
_⇒_ : Ty → Ty → Ty
data Con : Set where
∙ : Con
_,_ : Con → Ty → Con
data Tm : Con → Ty → Set
data Tms : Con → Con → Set where
_∘t_ : ∀{X Y Z} → Tms Y Z → Tms X Y → Tms X Z
Id : ∀{X} → Tms X X
ε : ∀{X} → Tms X ∙
_,_ : ∀{X Y A} → (p : Tms X Y) → Tm X A → Tms X (Y , A)
π₁ : ∀{X Y A} → Tms X (Y , A) → Tms X Y
data Tm where
_[_] : ∀{X Y A} → Tm X A → (p : Tms Y X) → Tm Y A
π₂ : ∀{X Y A} → (p : Tms X (Y , A)) → Tm X A
lam : ∀{X A B} → Tm (X , A) B → Tm X (A ⇒ B)
app : ∀{X A B} → Tm X (A ⇒ B) → Tm (X , A) B
wk : ∀{X A} → Tms (X , A) X
wk = π₁ Id
vz : ∀{X A} → Tm (X , A) A
vz = π₂ Id
vs : ∀{X A B} → Tm X A → Tm (X , B) A
vs x = x [ wk ]
<_> : ∀{Γ}{A : Ty} → Tm Γ A → Tms Γ (Γ , A)
< t > = Id , t
infixl 4 _$_
_$_ : ∀ {Γ}{A : Ty}{B : Ty}(t : Tm Γ (A ⇒ B))(u : Tm Γ A) → Tm Γ B
t $ u = (app t) [ < u > ]
[_⊢_] : Con → Ty → Set₁
[ X ⊢ base ] = Lift (suc zero) (Tm X base)
[ X ⊢ a ⇒ b ] = ∀ {Y} (s : Tms Y X) → [ Y ⊢ a ] → [ Y ⊢ b ]
reify : ∀{a X} → [ X ⊢ a ] → Tm X a
reflect : ∀{a X} → Tm X a → [ X ⊢ a ]
reify {base} (lift lower) = lower
reify {a ⇒ a₁} f = lam (reify (f (π₁ Id) (reflect vz)))
reflect {base} i = lift i
reflect {a ⇒ b} R s = reflect ∘ _$_ (R [ s ]) ∘ reify
data In : Con → Ty → Set where
Z : ∀{X x} → In (X , x) x
S : ∀{X x y} → In X x → In (X , y) x
[_⊢*_] : Con -> Con -> Set₁
[ X ⊢* Y ] = ∀{a} -> In Y a -> [ X ⊢ a ]
rename : ∀{X Y} (s : Tms Y X) {a} -> [ X ⊢ a ] -> [ Y ⊢ a ]
rename s {base} (lift l) = lift (l [ s ])
rename s {a ⇒ b} f t = f (s ∘t t)
extend : ∀{X Y a} -> [ Y ⊢* X ] -> [ Y ⊢ a ] -> [ Y ⊢* X , a ]
extend p x Z = x
extend p x (S z) = p z
inject : ∀{X a} → (x : In X a) → Tm X a
inject Z = vz
inject (S x) = vs (inject x)
id* : ∀ {X} -> [ X ⊢* X ]
id* = reflect ∘ inject
weaken : ∀{X Y A} → [ Y ⊢* X , A ] → [ Y ⊢* X ]
weaken x i = x (S i)
apply : ∀ {X W} (tms : Tms X W) {Y} → (p : [ Y ⊢* X ]) → [ Y ⊢* W ]
den : ∀{X a} -> Tm X a -> ∀ {Y} -> [ Y ⊢* X ] -> [ Y ⊢ a ]
apply (t ∘t v) p = apply t (apply v p)
apply Id p = p
apply (tms , x) p Z = den x p
apply (tms , x) p (S n) = apply tms p n
apply (π₁ tms) p n = apply tms p (S n)
den (M [ tms ]) p = den M (apply tms p)
den (π₂ tms) p = (apply tms p) Z
den (lam M) p s x = den M (extend (rename s ∘ p) x)
den (app M) p = den M (weaken p) Id (p Z)
normalize : ∀{X a} → Tm X a → Tm X a
normalize M = reify (den M id*)
cnat : Ty
cnat = (base ⇒ base) ⇒ base ⇒ base
czero : ∀{G} → Tm G cnat
czero = lam (π₂ Id)
csuc : ∀{G} → Tm G (cnat ⇒ cnat)
csuc = lam (lam (lam (vs vz $ (vs (vs vz) $ vs vz $ vz))))
ctwo : ∀{G} → Tm G cnat
ctwo = csuc $ (csuc $ czero)
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment