module A201901.Chapter5 where
open import A201901.Prelude public
hiding (false ; not ; suc ; true ; zero)
import A201901.Chapter3
record IsLC (Term : Set₀) : Set₀ where
infixl 7 _$_
field
ν : ∀ (x : Name) → Term
ƛ_∙_ : ∀ (x : Name) (t : Term) → Term
_$_ : ∀ (t₁ t₂ : Term) → Term
record LC : Set₁ where
field
Term : Set₀
isLC : IsLC Term
open IsLC isLC public
instance
Term-isString : IsString Term
Term-isString = record
{ Constraint = λ s → ⊤
; fromString = λ s → ν (name s)
}
module Church-Part1 (lc : LC)
where
open LC lc
tru = ƛ "t" ∙ ƛ "f" ∙ "t"
fls = ƛ "t" ∙ ƛ "f" ∙ "f"
test = ƛ "l" ∙ ƛ "m" ∙ ƛ "n" ∙ "l" $ "m" $ "n"
and = ƛ "b" ∙ ƛ "c" ∙ "b" $ "c" $ fls
or = ƛ "b" ∙ ƛ "c" ∙ "b" $ tru $ "c"
not = ƛ "b" ∙ "b" $ fls $ tru
pair = ƛ "f" ∙ ƛ "s" ∙ ƛ "b" ∙ "b" $ "f" $ "s"
fst = ƛ "p" ∙ "p" $ tru
snd = ƛ "p" ∙ "p" $ fls
c₀ = ƛ "s" ∙ ƛ "z" ∙ "z"
c₁ = ƛ "s" ∙ ƛ "z" ∙ "s" $ "z"
c₂ = ƛ "s" ∙ ƛ "z" ∙ "s" $ ("s" $ "z")
c₃ = ƛ "s" ∙ ƛ "z" ∙ "s" $ ("s" $ ("s" $ "z"))
sc = ƛ "n" ∙ ƛ "s" ∙ ƛ "z" ∙ "s" $ ("n" $ "s" $ "z")
sc2 = ƛ "n" ∙ ƛ "s" ∙ ƛ "z" ∙ "n" $ "s" $ ("s" $ "z")
plus = ƛ "m" ∙ ƛ "n" ∙ ƛ "s" ∙ ƛ "z" ∙ "m" $ "s" $ ("n" $ "s" $ "z")
times = ƛ "m" ∙ ƛ "n" ∙ "m" $ (plus $ "n") $ c₀
times2 = ƛ "m" ∙ ƛ "n" ∙ ƛ "s" ∙ ƛ "z" ∙ "m" $ ("n" $ "s") $ "z"
times3 = ƛ "m" ∙ ƛ "n" ∙ ƛ "s" ∙ "m" $ ("n" $ "s")
power = ƛ "n" ∙ ƛ "k" ∙ "k" $ (times $ "n") $ c₁
iszro = ƛ "m" ∙ "m" $ (ƛ "x" ∙ fls) $ tru
zz = pair $ c₀ $ c₀
ss = ƛ "p" ∙ pair $ (snd $ "p") $ (plus $ c₁ $ (snd $ "p"))
prd = ƛ "m" ∙ fst $ ("m" $ ss $ zz)
minus = ƛ "m" ∙ ƛ "n" ∙ "n" $ prd $ "m"
equal = ƛ "m" ∙ ƛ "n" ∙ and $ (iszro $ ("m" $ prd $ "n"))
$ (iszro $ ("n" $ prd $ "m"))
nil = ƛ "c" ∙ ƛ "n" ∙ "n"
cons = ƛ "h" ∙ ƛ "t" ∙ ƛ "c" ∙ ƛ "n" ∙ "c" $ "h" $ ("t" $ "c" $ "n")
isnil = ƛ "l" ∙ "l" $ (ƛ "h" ∙ ƛ "t" ∙ fls) $ tru
head = ƛ "l" ∙ "l" $ (ƛ "h" ∙ ƛ "t" ∙ "h") $ fls
tail = ƛ "l" ∙ fst $ "l" $ (ƛ "x" ∙ ƛ "p" ∙ pair $ (snd $ "p") $ (cons $ "x" $ (snd $ "p"))) $
(pair $ nil $ nil)
record IsLCNB (Term : Set₀) : Set₀ where
field
isLC : IsLC Term
true false zero : Term
suc pred iszero : ∀ (t : Term) → Term
if_then_else : ∀ (t₁ t₂ t₃ : Term) → Term
open IsLC isLC public
record LCNB : Set₁ where
field
Term : Set₀
isLCNB : IsLCNB Term
open IsLCNB isLCNB public
lc : LC
lc = record { isLC = isLC }
open LC lc public using (Term-isString)
module Church-Part2 (lcnb : LCNB)
where
open LCNB lcnb
open Church-Part1 lc
realbool = ƛ "b" ∙ "b" $ true $ false
churchbool = ƛ "b" ∙ if "b" then tru else fls
realeq = ƛ "m" ∙ ƛ "n" ∙ (equal $ "m" $ "n") $ true $ false
realnat = ƛ "m" ∙ "m" $ (ƛ "x" ∙ suc "x") $ zero
omega = (ƛ "x" ∙ "x" $ "x") $ (ƛ "x" ∙ "x" $ "x")
fix = ƛ "f" ∙ (ƛ "x" ∙ "f" $ (ƛ "y" ∙ "x" $ "x" $ "y")) $
(ƛ "x" ∙ "f" $ (ƛ "y" ∙ "x" $ "x" $ "y"))
f-step = ƛ "f" ∙ ƛ "n" ∙
if realeq $ "n" $ c₀
then c₁
else (times $ "n" $ ("f" $ (prd $ "n")))
factorial = fix $ f-step
f-step2 = ƛ "f" ∙ ƛ "n" ∙
test $ (iszro $ "n") $
(ƛ "x" ∙ c₁) $
(ƛ "x" ∙ (times $ "n" $ ("f" $ (prd $ "n")))) $ c₀
factorial2 = fix $ f-step2
cn-step = ƛ "f" ∙ ƛ "m" ∙
if iszero "m"
then c₀
else sc $ ("f" $ (pred "m"))
churchnat = fix $ cn-step
s-step = ƛ "f" ∙ ƛ "l" ∙
test $ (isnil $ "l") $
(ƛ "x" ∙ c₀) $
(ƛ "x" ∙ (plus $ (head $ "l") $ ("f" $ (tail $ "l")))) $ c₀
sum = fix $ s-step
open A201901.Prelude using (suc ; zero)
module Functions
where
infixl 7 _$_
data Term : Set₀ where
ν : ∀ (x : Name) → Term
ƛ_∙_ : ∀ (x : Name) (t : Term) → Term
_$_ : ∀ (t₁ t₂ : Term) → Term
Functions-lc : LC
Functions-lc = record
{ Term = Term
; isLC = record
{ ν = ν
; ƛ_∙_ = ƛ_∙_
; _$_ = _$_
}
}
size : Term → Nat
size (ν x) = 1
size (ƛ x ∙ t) = 1 + size t
size (t₁ $ t₂) = 1 + (size t₁ + size t₂)
size-positive : ∀ t → 1 ≤ size t
size-positive (ν x) = ≤-refl
size-positive (ƛ x ∙ t) = s≤s z≤n
size-positive (t₁ $ t₂) = s≤s z≤n
infix 5 _<ˢ_
_<ˢ_ : Rel₀ Term
_<ˢ_ = _<_ on size
<ˢ-abs : ∀ x t → t <ˢ ƛ x ∙ t
<ˢ-abs x t = ≤-refl
<ˢ-abs′ : ∀ x t t′ → size t ≡ size t′ → t′ <ˢ ƛ x ∙ t
<ˢ-abs′ x t t′ s≡s′ = begin
suc (size t′)
≡⟨ suc & (s≡s′ ⁻¹) ⟩
suc (size t)
∎
<ˢ-app₁ : ∀ t₁ t₂ → t₁ <ˢ t₁ $ t₂
<ˢ-app₁ t₁ t₂ = ≤-step
(begin
suc (size t₁)
≤⟨ +-monoˡ-≤ (size t₁) (size-positive t₂) ⟩
size t₂ + size t₁
≡⟨ +-comm (size t₂) (size t₁) ⟩
size t₁ + size t₂
∎)
<ˢ-app₂ : ∀ t₁ t₂ → t₂ <ˢ t₁ $ t₂
<ˢ-app₂ t₁ t₂ = ≤-step
(begin
suc (size t₂)
≤⟨ +-monoˡ-≤ (size t₂) (size-positive t₁) ⟩
size t₁ + size t₂
∎)
<ˢ-wellFounded : WellFounded _<ˢ_
<ˢ-wellFounded = InverseImage.wellFounded size <-wellFounded
indSize : ∀ {ℓ} {P : Pred Term ℓ} → InductionPrinciple _<ˢ_ P
indSize = indWith <ˢ-wellFounded
_≟ᵀ_ : Decidable {A = Term} _≡_
(ν x) ≟ᵀ (ν y) with x ≟ᴺ y
... | no x≢y = no λ where refl → refl ↯ x≢y
... | yes refl = yes refl
(ν x) ≟ᵀ (ƛ y ∙ u) = no λ ()
(ν x) ≟ᵀ (u₁ $ u₂) = no λ ()
(ƛ x ∙ t) ≟ᵀ (ν y) = no λ ()
(ƛ x ∙ t) ≟ᵀ (ƛ y ∙ u) with x ≟ᴺ y | t ≟ᵀ u
... | no x≢y | _ = no λ where refl → refl ↯ x≢y
... | yes refl | no t≢u = no λ where refl → refl ↯ t≢u
... | yes refl | yes refl = yes refl
(ƛ x ∙ t) ≟ᵀ (u₁ $ u₂) = no λ ()
(t₁ $ t₂) ≟ᵀ (ν y) = no λ ()
(t₁ $ t₂) ≟ᵀ (ƛ y ∙ u) = no λ ()
(t₁ $ t₂) ≟ᵀ (u₁ $ u₂) with t₁ ≟ᵀ u₁ | t₂ ≟ᵀ u₂
... | no t₁≢u₁ | _ = no λ where refl → refl ↯ t₁≢u₁
... | yes refl | no t₂≢u₂ = no λ where refl → refl ↯ t₂≢u₂
... | yes refl | yes refl = yes refl
Term-hasDecidableEquality : HasDecidableEquality Term
Term-hasDecidableEquality = record { _≟_ = _≟ᵀ_ }
fv : Term → UniqueList Name
fv (ν x) = [ x ]
fv (ƛ x ∙ t) = fv t ∖ [ x ]
fv (t₁ $ t₂) = fv t₁ ∪ fv t₂
exe533 : ∀ t → length (fv t) ≤ size t
exe533 (ν x) = ≤-refl
exe533 (ƛ x ∙ t) = ≤-step
(begin
length (fv t ∖ [ x ])
≤⟨ length-untitled (fv t) [ x ] ⟩
length (fv t)
≤⟨ exe533 t ⟩
size t
∎)
exe533 (t₁ $ t₂) = ≤-step
(begin
length (fv t₁ ∪ fv t₂)
≤⟨ length-triangular (fv t₁) (fv t₂) ⟩
length (fv t₁) + length (fv t₂)
≤⟨ +-mono-≤ (exe533 t₁) (exe533 t₂) ⟩
size t₁ + size t₂
∎)
postulate
fresh : UniqueList Name → Name
private
module NotGood where
{-# TERMINATING #-}
[_↦_]_ : Name → Term → Term → Term
[ x ↦ s ] (ν y) with x ≟ᴺ y
... | yes refl = s
... | no x≢y = ν y
[ x ↦ s ] (ƛ y ∙ t) with x ≟ᴺ y | fv s T⟨∌⟩? x
... | yes refl | _ = ƛ y ∙ t
... | no x≢y | yes T⟨fvs∌x⟩ = ƛ y ∙ [ x ↦ s ] t
... | no x≢y | no ¬T⟨fvs∌x⟩ = let z = fresh (fv s ∪ fv t) in
ƛ z ∙ [ x ↦ s ] ([ y ↦ ν z ] t)
[ x ↦ s ] (t₁ $ t₂) = ([ x ↦ s ] t₁) $ ([ x ↦ s ] t₂)
c-ren : Closed _<ˢ_ (λ t → Name → Name → ∃ λ t′ → size t ≡ size t′)
c-ren (ν y) h x z with x ≟ᴺ y
... | yes refl = ν z , refl
... | no x≢y = ν y , refl
c-ren (ƛ y ∙ t) h x z with x ≟ᴺ y
... | yes refl = ƛ y ∙ t , refl
... | no x≢y = let (t′ , s≡s′) = h t (<ˢ-abs x t) x z in
ƛ y ∙ t′ , suc & s≡s′
c-ren (t₁ $ t₂) h x z = let (t₁′ , s₁≡s₁′) = h t₁ (<ˢ-app₁ t₁ t₂) x z
(t₂′ , s₂≡s₂′) = h t₂ (<ˢ-app₂ t₁ t₂) x z in
t₁′ $ t₂′ , (λ s₁ s₂ → suc (s₁ + s₂)) & s₁≡s₁′ ⊗ s₂≡s₂′
ren : ∀ (t : Term) → Name → Name → ∃ λ t′ → size t ≡ size t′
ren = indSize c-ren
c-sub : Closed _<ˢ_ (λ t → Name → Term → Term)
c-sub (ν y) h x s with x ≟ᴺ y
... | yes refl = s
... | no x≢y = ν y
c-sub (ƛ y ∙ t) h x s with x ≟ᴺ y | fv s T⟨∌⟩? x
... | yes refl | _ = ƛ y ∙ t
... | no x≢y | yes T⟨fvs∌x⟩ = ƛ y ∙ h t (<ˢ-abs x t) x s
... | no x≢y | no ¬T⟨fvs∌x⟩ = let z = fresh (fv s ∪ fv t)
(t′ , s≡s′) = ren t y z in
ƛ z ∙ h t′ (<ˢ-abs′ x t t′ s≡s′) x s
c-sub (t₁ $ t₂) h x s = h t₁ (<ˢ-app₁ t₁ t₂) x s $ h t₂ (<ˢ-app₂ t₁ t₂) x s
sub : ∀ (t : Term) → Name → Term → Term
sub = indSize c-sub
[_↦_]_ : Name → Term → Term → Term
[ x ↦ s ] t = sub t x s
{-# DISPLAY c-sub t _ x s = [ x ↦ s ] t #-}
module FunctionsGetStuck
where
open Functions public
data Value : Pred₀ Term where
ƛ_∙_ : ∀ (x : Name) (t : Term) → Value (ƛ x ∙ t)
infix 3 _⇒_
data _⇒_ : Rel₀ Term where
r-app₁ : ∀ {t₁ t₂ u₁} → t₁ ⇒ u₁ → t₁ $ t₂ ⇒ u₁ $ t₂
r-app₂ : ∀ {t₁ t₂ u₂} → (vₜ₁ : Value t₁) → t₂ ⇒ u₂ → t₁ $ t₂ ⇒ t₁ $ u₂
r-appAbs : ∀ {x t₁ t₂} → (vₜ₂ : Value t₂) → (ƛ x ∙ t₁) $ t₂ ⇒ [ x ↦ t₂ ] t₁
open A201901.Chapter3.NormalForms _⇒_ public
v→nf : ∀ {t} → Value t → NormalForm t
v→nf (ƛ x ∙ t) = λ ()
⇒-det : ∀ {t u u′} → t ⇒ u → t ⇒ u′ → u ≡ u′
⇒-det (r-app₁ t₁⇒u₁) (r-app₁ t₁⇒u₁′) = (_$ _) & ⇒-det t₁⇒u₁ t₁⇒u₁′
⇒-det (r-app₁ t₁⇒u₁) (r-app₂ vₜ₁ _) = t₁⇒u₁ ↯ v→nf vₜ₁
⇒-det (r-app₁ ()) (r-appAbs _)
⇒-det (r-app₂ vₜ₁ _) (r-app₁ t₁⇒u₁) = t₁⇒u₁ ↯ v→nf vₜ₁
⇒-det (r-app₂ vₜ₁ t₂⇒u₂) (r-app₂ vₜ₂ t₂⇒u₂′) = (_ $_) & ⇒-det t₂⇒u₂ t₂⇒u₂′
⇒-det (r-app₂ _ t₂⇒u₂) (r-appAbs vₜ₂) = t₂⇒u₂ ↯ v→nf vₜ₂
⇒-det (r-appAbs _) (r-app₁ ())
⇒-det (r-appAbs vₜ₂) (r-app₂ _ t₂⇒u₂) = t₂⇒u₂ ↯ v→nf vₜ₂
⇒-det (r-appAbs vₜ₂) (r-appAbs vₜ₂′) = refl
Stuck : Pred₀ Term
Stuck t = ¬ Value t × NormalForm t
data Stuck/Value/Reducible : Pred₀ Term where
stu : ∀ {t} → (σₜ : Stuck t) → Stuck/Value/Reducible t
val : ∀ {t} → (vₜ : Value t) → Stuck/Value/Reducible t
red : ∀ {t} → (rₜ : Reducible t) → Stuck/Value/Reducible t
σ-appStuck₁ : ∀ {t₁ t₂} → Stuck t₁ → Stuck (t₁ $ t₂)
σ-appStuck₁ (¬vₜ₁ , nfₜ₁) = (λ ())
, (λ where (r-app₁ t₁⇒u₁) → t₁⇒u₁ ↯ nfₜ₁
(r-app₂ vₜ₁ t₂⇒u₂) → vₜ₁ ↯ ¬vₜ₁
(r-appAbs vₜ₂) → (ƛ _ ∙ _) ↯ ¬vₜ₁)
σ-appStuck₂ : ∀ {t₁ t₂} → Value t₁ → Stuck t₂ → Stuck (t₁ $ t₂)
σ-appStuck₂ vₜ₁ (¬vₜ₂ , nfₜ₂) = (λ ())
, (λ where (r-app₁ t₁⇒u₁) → t₁⇒u₁ ↯ v→nf vₜ₁
(r-app₂ vₜ₁ t₂⇒u₂) → t₂⇒u₂ ↯ nfₜ₂
(r-appAbs vₜ₂) → vₜ₂ ↯ ¬vₜ₂)
classify : ∀ t → Stuck/Value/Reducible t
classify (ν x) = stu ((λ ()) , (λ ()))
classify (ƛ x ∙ t) = val (ƛ x ∙ t)
classify (t₁ $ t₂) with classify t₁ | classify t₂
... | stu σₜ₁ | _ = stu (σ-appStuck₁ σₜ₁)
... | val vₜ₁ | stu σₜ₂ = stu (σ-appStuck₂ vₜ₁ σₜ₂)
... | val (ƛ _ ∙ _) | val vₜ₂ = red (_ , r-appAbs vₜ₂)
... | val vₜ₁ | red (_ , t₂⇒u₂) = red (_ , r-app₂ vₜ₁ t₂⇒u₂)
... | red (_ , t₁⇒u₁) | _ = red (_ , r-app₁ t₁⇒u₁)
data Stuck/Value : Pred₀ Term where
stu : ∀ {t} → (σₜ : Stuck t) → Stuck/Value t
val : ∀ {t} → (vₜ : Value t) → Stuck/Value t
nf→σ/v : ∀ {t} → NormalForm t → Stuck/Value t
nf→σ/v {t} nfₜ with classify t
... | stu σₜ = stu σₜ
... | val vₜ = val vₜ
... | red (_ , t⇒u) = t⇒u ↯ nfₜ
open A201901.Chapter3.MultiStepReduction _⇒_ public
open A201901.Chapter3.UniquenessOfNormalForms _⇒_ ⇒-det public
rs-app₁ : ∀ {t₁ t₂ u₁} → t₁ ⇒* u₁ → t₁ $ t₂ ⇒* u₁ $ t₂
rs-app₁ = map r-app₁
rs-app₂ : ∀ {t₁ t₂ u₂} → (vₜ₁ : Value t₁) → t₂ ⇒* u₂ → t₁ $ t₂ ⇒* t₁ $ u₂
rs-app₂ vₜ₁ = map (r-app₂ vₜ₁)
rs-appAbs : ∀ {x t₁ t₂} → (vₜ₂ : Value t₂) → (ƛ x ∙ t₁) $ t₂ ⇒* [ x ↦ t₂ ] t₁
rs-appAbs vₜ₂ = r-appAbs vₜ₂ ◅ ε
module Strategy-FullBetaReduction
where
open Functions public
infix 3 _⇒_
data _⇒_ : Rel₀ Term where
r-app₁ : ∀ {t₁ t₂ u₁} → t₁ ⇒ u₁ → t₁ $ t₂ ⇒ u₁ $ t₂
r-app₂ : ∀ {t₁ t₂ u₂} → t₂ ⇒ u₂ → t₁ $ t₂ ⇒ t₁ $ u₂
r-abs : ∀ {x t u} → t ⇒ u → ƛ x ∙ t ⇒ ƛ x ∙ u
r-appAbs : ∀ {x t₁ t₂} → (ƛ x ∙ t₁) $ t₂ ⇒ [ x ↦ t₂ ] t₁
open A201901.Chapter3.NormalForms _⇒_ public
module Strategy-NormalOrder
where
open Functions public
mutual
data NormalForm : Pred₀ Term where
ƛ_∙_ : ∀ x {t} → (nfₜ : NormalForm t) → NormalForm (ƛ x ∙ t)
nanf : ∀ {t} → (nanfₜ : NonAbstractionNormalForm t) → NormalForm t
data NonAbstractionNormalForm : Pred₀ Term where
ν : ∀ x → NonAbstractionNormalForm (ν x)
_$_ : ∀ {t₁ t₂} → (nanfₜ₁ : NonAbstractionNormalForm t₁) (nfₜ₂ : NormalForm t₂) →
NonAbstractionNormalForm (t₁ $ t₂)
data NonAbstraction : Pred₀ Term where
ν : ∀ x → NonAbstraction (ν x)
_$_ : ∀ t₁ t₂ → NonAbstraction (t₁ $ t₂)
infix 3 _⇒_
data _⇒_ : Rel₀ Term where
r-app₁ : ∀ {t₁ t₂ u₁} → (naₜ₁ : NonAbstraction t₁) (naᵤ₁ : NonAbstraction u₁) → t₁ ⇒ u₁ →
t₁ $ t₂ ⇒ u₁ $ t₂
r-app₂ : ∀ {t₁ t₂ u₂} → (nanfₜ₁ : NonAbstractionNormalForm t₁) → t₂ ⇒ u₂ → t₁ $ t₂ ⇒ t₁ $ u₂
r-abs : ∀ {x t u} → t ⇒ u → ƛ x ∙ t ⇒ ƛ x ∙ u
r-appAbs : ∀ {x t₁ t₂} → (ƛ x ∙ t₁) $ t₂ ⇒ [ x ↦ t₂ ] t₁
open A201901.Chapter3.NormalForms _⇒_ public
renaming (NormalForm to NegativeNormalForm ; nf→¬r to nnf→¬r ; ¬r→nf to ¬r→nnf)
mutual
nf→nnf : ∀ {t} → NormalForm t → NegativeNormalForm t
nf→nnf (ƛ _ ∙ nfₜ) = λ where (r-abs t⇒u) → t⇒u ↯ nf→nnf nfₜ
nf→nnf (nanf nanfₜ) = nanf→nnf nanfₜ
nanf→nnf : ∀ {t} → NonAbstractionNormalForm t → NegativeNormalForm t
nanf→nnf (ν _) = λ ()
nanf→nnf (nanfₜ₁ $ nfₜ₂) = λ where
(r-app₁ naₜ₁ naᵤ₁ t₁⇒u₁) → t₁⇒u₁ ↯ nanf→nnf nanfₜ₁
(r-app₂ nanfₜ₁ t₂⇒u₂) → t₂⇒u₂ ↯ nf→nnf nfₜ₂
r-appAbs → case nanfₜ₁ of λ where ()
⇒-det : ∀ {t u u′} → t ⇒ u → t ⇒ u′ → u ≡ u′
⇒-det (r-app₁ _ _ t₁⇒u₁) (r-app₁ _ _ t₁⇒u₁′) = (_$ _) & ⇒-det t₁⇒u₁ t₁⇒u₁′
⇒-det (r-app₁ _ _ t₁⇒u₁) (r-app₂ nanfₜ₁ _) = t₁⇒u₁ ↯ nanf→nnf nanfₜ₁
⇒-det (r-app₁ () _ _) r-appAbs
⇒-det (r-app₂ nanfₜ₁ _) (r-app₁ _ _ t₁⇒u₁′) = t₁⇒u₁′ ↯ nanf→nnf nanfₜ₁
⇒-det (r-app₂ _ t₂⇒u₂) (r-app₂ _ t₂⇒u₂′) = (_ $_) & ⇒-det t₂⇒u₂ t₂⇒u₂′
⇒-det (r-app₂ () _) r-appAbs
⇒-det (r-abs t⇒u) (r-abs t⇒u′) = (ƛ _ ∙_) & ⇒-det t⇒u t⇒u′
⇒-det r-appAbs (r-app₁ () _ _)
⇒-det r-appAbs (r-app₂ () _)
⇒-det r-appAbs r-appAbs = refl
open A201901.Chapter3.MultiStepReduction _⇒_ public
open A201901.Chapter3.UniquenessOfNormalForms _⇒_ ⇒-det public
module Strategy-Lazy/CallByName
where
open Functions public
infix 3 _⇒_
data _⇒_ : Rel₀ Term where
r-app₁ : ∀ {t₁ t₂ u₁} → t₁ ⇒ u₁ → t₁ $ t₂ ⇒ u₁ $ t₂
r-appAbs : ∀ {x t₁ t₂} → (ƛ x ∙ t₁) $ t₂ ⇒ [ x ↦ t₂ ] t₁
data Value : Pred₀ Term where
ƛ_∙_ : ∀ (x : Name) (t : Term) → Value (ƛ x ∙ t)
open A201901.Chapter3.NormalForms _⇒_ public
v→nf : ∀ {t} → Value t → NormalForm t
v→nf (ƛ x ∙ t) = λ ()
⇒-det : ∀ {t u u′} → t ⇒ u → t ⇒ u′ → u ≡ u′
⇒-det (r-app₁ t₁⇒u₁) (r-app₁ t₁⇒u₁′) = (_$ _) & ⇒-det t₁⇒u₁ t₁⇒u₁′
⇒-det (r-app₁ ()) r-appAbs
⇒-det r-appAbs (r-app₁ ())
⇒-det r-appAbs r-appAbs = refl
open A201901.Chapter3.MultiStepReduction _⇒_ public
open A201901.Chapter3.UniquenessOfNormalForms _⇒_ ⇒-det public
private
module Exercise538 where
open FunctionsGetStuck
infix 3 _⇓_
data _⇓_ : Rel₀ Term where
e-val : ∀ {t} → (vₜ : Value t) → t ⇓ t
e-appAbs : ∀ {x t₁ t₂ u₁ u₂ u} → (vᵤ₂ : Value u₂) → t₁ ⇓ ƛ x ∙ u₁ → t₂ ⇓ u₂ → [ x ↦ u₂ ] u₁ ⇓ u →
t₁ $ t₂ ⇓ u
exe568-ltr : ∀ {t u} → (vᵤ : Value u) → t ⇓ u → t ⇒* u
exe568-ltr vᵤ (e-val vₜ)
= ε
exe568-ltr vᵤ (e-appAbs vᵤ₂ t₁⇓ƛx∙u₁ t₂⇓u₂ [x↦u₂]u₁⇓u)
= rs-app₁ (exe568-ltr (ƛ _ ∙ _) t₁⇓ƛx∙u₁) ◅◅
rs-app₂ (ƛ _ ∙ _) (exe568-ltr vᵤ₂ t₂⇓u₂) ◅◅
rs-appAbs vᵤ₂ ◅◅
(exe568-ltr vᵤ [x↦u₂]u₁⇓u)
lem-app₁ : ∀ {t₁ t₂ u} → (vᵤ : Value u) → t₁ $ t₂ ⇒* u →
∃ λ x → ∃ λ u₁ → ∃ λ u₂ → Value u₂ × t₁ ⇒* ƛ x ∙ u₁ × t₂ ⇒* u₂ × [ x ↦ u₂ ] u₁ ⇒* u
lem-app₁ () ε
lem-app₁ vᵤ (r-app₁ t₁⇒i₁ ◅ i₁$t₂⇒*u) with lem-app₁ vᵤ i₁$t₂⇒*u
... | x , u₁ , u₂ , vᵤ₂ , i₁⇒*ƛx∙u₁ , t₂⇒*u₂ , [x↦u₂]u₁⇒*u
= x , u₁ , u₂ , vᵤ₂ , t₁⇒i₁ ◅ i₁⇒*ƛx∙u₁ , t₂⇒*u₂ , [x↦u₂]u₁⇒*u
lem-app₁ vᵤ (r-app₂ vₜ₁ t₂⇒i₂ ◅ t₁$i₂⇒*u) with lem-app₁ vᵤ t₁$i₂⇒*u
... | x , u₁ , u₂ , vᵤ₂ , t₁⇒*ƛx∙u₁ , i₂⇒*u₂ , [x↦u₂]u₁⇒*u
= x , u₁ , u₂ , vᵤ₂ , t₁⇒*ƛx∙u₁ , t₂⇒i₂ ◅ i₂⇒*u₂ , [x↦u₂]u₁⇒*u
lem-app₁ vᵤ (r-appAbs {x} {t₁} vₜ₂ ◅ [x↦t₂]t₁⇒*u)
= x , t₁ , _ , vₜ₂ , ε , ε , [x↦t₂]t₁⇒*u
lem-app₂ : ∀ {x t₂ u u₁} → (vᵤ : Value u) → ƛ x ∙ u₁ $ t₂ ⇒* u →
∃ λ u₂ → Value u₂ × t₂ ⇒* u₂ × [ x ↦ u₂ ] u₁ ⇒* u
lem-app₂ () ε
lem-app₂ vᵤ (r-app₁ () ◅ _)
lem-app₂ vᵤ (r-app₂ vₜ₁ t₂⇒i₂ ◅ t₁$i₂⇒*u) with lem-app₂ vᵤ t₁$i₂⇒*u
... | u₂ , vᵤ₂ , i₂⇒*u₂ , [x↦u₂]t₁⇒*u
= u₂ , vᵤ₂ , t₂⇒i₂ ◅ i₂⇒*u₂ , [x↦u₂]t₁⇒*u
lem-app₂ vᵤ (r-appAbs vₜ₂ ◅ [x↦t₂]t₁⇒*u)
= _ , vₜ₂ , ε , [x↦t₂]t₁⇒*u
private
module NotGood where
{-# TERMINATING #-}
exe568-rtl : ∀ {t u} → (vᵤ : Value u) → t ⇒* u → t ⇓ u
exe568-rtl vᵤ ε
= e-val vᵤ
exe568-rtl vᵤ (r-app₁ t₁⇒i₁ ◅ i₁$t₂⇒*u) with lem-app₁ vᵤ i₁$t₂⇒*u
... | x , u₁ , u₂ , vᵤ₂ , i₁⇒*ƛx∙u₁ , t₂⇒*u₂ , [x↦u₂]u₁⇒*u
= e-appAbs vᵤ₂ (exe568-rtl (ƛ _ ∙ _) (t₁⇒i₁ ◅ i₁⇒*ƛx∙u₁))
(exe568-rtl vᵤ₂ t₂⇒*u₂)
(exe568-rtl vᵤ [x↦u₂]u₁⇒*u)
exe568-rtl vᵤ (r-app₂ vₜ₁@(ƛ _ ∙ _) t₂⇒i₂ ◅ t₁$i₂⇒*u) with lem-app₂ vᵤ t₁$i₂⇒*u
... | u₂ , vᵤ₂ , i₂⇒*u₂ , [x↦u₂]u₁⇒*u
= e-appAbs vᵤ₂ (e-val vₜ₁)
(exe568-rtl vᵤ₂ (t₂⇒i₂ ◅ i₂⇒*u₂))
(exe568-rtl vᵤ [x↦u₂]u₁⇒*u)
exe568-rtl vᵤ (r-appAbs vₜ₂ ◅ [x↦t₂]t₁⇒*u)
= e-appAbs vₜ₂ (e-val (ƛ _ ∙ _))
(e-val vₜ₂)
(exe568-rtl vᵤ [x↦t₂]t₁⇒*u)
exe568 : ∀ {t u} → (vᵤ : Value u) → (t ⇓ u) ↔ (t ⇒* u)
exe568 vᵤ = exe568-ltr vᵤ , exe568-rtl vᵤ