2.3. Named Reduction Rules
The relation ReduceIn presents beta reduction directly over named syntax.
Its substitution premise is still checked by translating the redex to L0,
which avoids implementing a separate fresh-name algorithm here.
\frac{[e_2/x]e_1 = e'}{(\lambda x.\ e_1)\ e_2 \longrightarrow e'}
\qquad
\frac{e \longrightarrow e'}{\lambda x.\ e \longrightarrow \lambda x.\ e'}
\frac{e_1 \longrightarrow e_1'}{e_1\ e_2 \longrightarrow e_1'\ e_2}
\qquad
\frac{e_2 \longrightarrow e_2'}{e_1\ e_2 \longrightarrow e_1\ e_2'}
These rules are the named presentation of reduction. The beta rule delegates
the substitution check to L0, and the soundness theorem below connects
the named relation back to beta reduction on meanings.
def SubstIn (ρ : List String) (x : String) (arg body out : L1) : Prop :=
L0.subst 0 (toL0With ρ arg) (toL0With (x :: ρ) body) = toL0With ρ outdef Subst (x : String) (arg body out : L1) : Prop :=
SubstIn [] x arg body outinductive ReduceIn : List String -> L1 -> L1 -> Prop where
| beta :
SubstIn ρ x arg body out ->
ReduceIn ρ (.app (.lam x body) arg) out
| lam :
ReduceIn (x :: ρ) body body' ->
ReduceIn ρ (.lam x body) (.lam x body')
| app_left :
ReduceIn ρ fn fn' ->
ReduceIn ρ (.app fn arg) (.app fn' arg)
| app_right :
ReduceIn ρ arg arg' ->
ReduceIn ρ (.app fn arg) (.app fn arg')def Reduce : L1 -> L1 -> Prop := ReduceIn []def ReduceStar : L1 -> L1 -> Prop := Relation.ReflTransGen Reducetheorem StepIn.toBetaStep : ReduceIn ρ e e' -> L1.toL0With ρ e →β₀ L1.toL0With ρ e' := ρ:List Stringe:L1e':L1⊢ ReduceIn ρ e e' → toL0With ρ e →β₀ toL0With ρ e'
ρ:List Stringe:L1e':L1h:ReduceIn ρ e e'⊢ toL0With ρ e →β₀ toL0With ρ e'; ρ:List Stringe:L1e':L1ρ✝:List Stringx✝:Stringarg✝:L1body✝:L1out✝:L1a✝:SubstIn ρ✝ x✝ arg✝ body✝ out✝⊢ toL0With ρ✝ ((lam x✝ body✝).app arg✝) →β₀ toL0With ρ✝ out✝ρ:List Stringe:L1e':L1x✝:Stringρ✝:List Stringbody✝:L1body'✝:L1a✝:ReduceIn (x✝ :: ρ✝) body✝ body'✝a_ih✝:toL0With (x✝ :: ρ✝) body✝ →β₀ toL0With (x✝ :: ρ✝) body'✝⊢ toL0With ρ✝ (lam x✝ body✝) →β₀ toL0With ρ✝ (lam x✝ body'✝)ρ:List Stringe:L1e':L1ρ✝:List Stringfn✝:L1fn'✝:L1arg✝:L1a✝:ReduceIn ρ✝ fn✝ fn'✝a_ih✝:toL0With ρ✝ fn✝ →β₀ toL0With ρ✝ fn'✝⊢ toL0With ρ✝ (fn✝.app arg✝) →β₀ toL0With ρ✝ (fn'✝.app arg✝)ρ:List Stringe:L1e':L1ρ✝:List Stringarg✝:L1arg'✝:L1fn✝:L1a✝:ReduceIn ρ✝ arg✝ arg'✝a_ih✝:toL0With ρ✝ arg✝ →β₀ toL0With ρ✝ arg'✝⊢ toL0With ρ✝ (fn✝.app arg✝) →β₀ toL0With ρ✝ (fn✝.app arg'✝) ρ:List Stringe:L1e':L1ρ✝:List Stringx✝:Stringarg✝:L1body✝:L1out✝:L1a✝:SubstIn ρ✝ x✝ arg✝ body✝ out✝⊢ toL0With ρ✝ ((lam x✝ body✝).app arg✝) →β₀ toL0With ρ✝ out✝ρ:List Stringe:L1e':L1x✝:Stringρ✝:List Stringbody✝:L1body'✝:L1a✝:ReduceIn (x✝ :: ρ✝) body✝ body'✝a_ih✝:toL0With (x✝ :: ρ✝) body✝ →β₀ toL0With (x✝ :: ρ✝) body'✝⊢ toL0With ρ✝ (lam x✝ body✝) →β₀ toL0With ρ✝ (lam x✝ body'✝)ρ:List Stringe:L1e':L1ρ✝:List Stringfn✝:L1fn'✝:L1arg✝:L1a✝:ReduceIn ρ✝ fn✝ fn'✝a_ih✝:toL0With ρ✝ fn✝ →β₀ toL0With ρ✝ fn'✝⊢ toL0With ρ✝ (fn✝.app arg✝) →β₀ toL0With ρ✝ (fn'✝.app arg✝)ρ:List Stringe:L1e':L1ρ✝:List Stringarg✝:L1arg'✝:L1fn✝:L1a✝:ReduceIn ρ✝ arg✝ arg'✝a_ih✝:toL0With ρ✝ arg✝ →β₀ toL0With ρ✝ arg'✝⊢ toL0With ρ✝ (fn✝.app arg✝) →β₀ toL0With ρ✝ (fn✝.app arg'✝) All goals completed! 🐙theorem Step.toBetaStep : Reduce e e' -> L1.toL0 e →β₀ L1.toL0 e' :=
@StepIn.toBetaStep [] _ _theorem Reduce.sound: Reduce e e' -> e →β₁ e' :=
Step.toBetaSteptheorem ReduceStar.sound : ReduceStar e e' -> e →β₁* e' := e:L1e':L1⊢ e.ReduceStar e' → e →β₁* e'
e:L1e':L1h:e.ReduceStar e'⊢ e →β₁* e'; e:L1e':L1⊢ e →β₁* ee:L1e':L1b✝:L1c✝:L1a✝¹:Relation.ReflTransGen Reduce e b✝a✝:b✝.Reduce c✝a_ih✝:e →β₁* b✝⊢ e →β₁* c✝ e:L1e':L1⊢ e →β₁* ee:L1e':L1b✝:L1c✝:L1a✝¹:Relation.ReflTransGen Reduce e b✝a✝:b✝.Reduce c✝a_ih✝:e →β₁* b✝⊢ e →β₁* c✝ All goals completed! 🐙infix:50 " ⟶₁ " => Reduceinfix:50 " ⟶₁* " => ReduceStar