Confluence by Z in Agda for PLFA
Vincent van Oostrom
University of Sussex

vvo@sussex.ac.uk

IWC, Tallinn, Estonia July 9th 20240

Pen-and-paper confluence of λβ (cf. Barendregt 84)
Definition (λ-term; Church 32)
A λ-term either is a variable x or an application M N or a λ-abstraction λx.M

IWC, Tallinn, Estonia July 9th 20241

Pen-and-paper confluence of λβDefinition (λ-term)
A λ-term either is a variable x or an application M N or a λ-abstraction λx.M

λ-terms up to α-congruence induced by λx.M = λy.M[x:=y], for y not in M

IWC, Tallinn, Estonia July 9th 20241

Pen-and-paper confluence of λβDefinition (λ-term)
A λ-term either is a variable x or an application M N or a λ-abstraction λx.M

λ-terms up to α-congruence induced by λx.M = λy.M[x:=y], for y not in M
Definition (β -reduction)→β on λ-terms is compatible closure of β -scheme (λx.M) N = M[x:=N]

IWC, Tallinn, Estonia July 9th 20241

Pen-and-paper confluence of λβDefinition (λ-term)
A λ-term either is a variable x or an application M N or a λ-abstraction λx.M

λ-terms up to α-congruence induced by λx.M = λy.M[x:=y], for y not in M
Definition (β -reduction)→β on λ-terms is compatible closure of β -scheme (λx.M) N = M[x:=N]
M[x:=N] the capture-avoiding substitution of N for x in M

IWC, Tallinn, Estonia July 9th 20241

Pen-and-paper confluence of λβDefinition (λ-term)
A λ-term either is a variable x or an application M N or a λ-abstraction λx.M

λ-terms up to α-congruence induced by λx.M = λy.M[x:=y], for y not in M
Definition (β -reduction)→β on λ-terms is compatible closure of β -scheme (λx.M) N = M[x:=N]
M[x:=N] the capture-avoiding substitution of N for x in M
Theorem (Church–Rosser 36)→β has the Church–Rosser property

IWC, Tallinn, Estonia July 9th 20241

Pen-and-paper confluence of λβDefinition (λ-term)
A λ-term either is a variable x or an application M N or a λ-abstraction λx.M

λ-terms up to α-congruence induced by λx.M = λy.M[x:=y], for y not in M
Definition (β -reduction)→β on λ-terms is compatible closure of β -scheme (λx.M) N = M[x:=N]
M[x:=N] the capture-avoiding substitution of N for x in M
Theorem (Church–Rosser)→β has the Church–Rosser property⇐⇒ →β is confluent ⇐⇒ ↠β has the diamond property
IWC, Tallinn, Estonia July 9th 2024

1

Z
Definition (Z-property of → for bullet-function • on objects)
a

b

a•

IWC, Tallinn, Estonia July 9th 2024

b•

2

Z
Definition (Z-property of → for •; Loader 98, Dehornoy &08)

for every step a → b(upperbound) b ↠ a•(monotonic) a• ↠ b•

IWC, Tallinn, Estonia July 9th 2024

2

Z
Definition (Z-property of → for •)abupperbounda•b•monotonic

IWC, Tallinn, Estonia July 9th 2024

2

Z
Definition (Z-property of → for •)for every step a → b, both b ↠ a• (ub) and a• ↠ b• (mon)Lemma (Z =⇒ strip =⇒ confluence (Barendregt 84))

strip

IWC, Tallinn, Estonia July 9th 2024

2

Z
Definition (Z-property of → for •)for every step a → b, both b ↠ a• (ub) and a• ↠ b• (mon)Lemma (Z =⇒ strip =⇒ confluence)
a

b

a′

IWC, Tallinn, Estonia July 9th 2024

2

Z
Definition (Z-property of → for •)for every step a → b, both b ↠ a• (ub) and a• ↠ b• (mon)Lemma (Z =⇒ strip =⇒ confluence)
a

a′

ub

IWC, Tallinn, Estonia July 9th 2024

b

a•

2

Z
Definition (Z-property of → for •)for every step a → b, both b ↠ a• (ub) and a• ↠ b• (mon)Lemma (Z =⇒ strip =⇒ confluence)
a

b
Z

a′

IWC, Tallinn, Estonia July 9th 2024

a•

b•

2

Z
Definition (Z-property of → for •)for every step a → b, both b ↠ a• (ub) and a• ↠ b• (mon)Lemma (Z =⇒ strip =⇒ confluence)

Z

IWC, Tallinn, Estonia July 9th 2024

2

Z
Definition (Z-property of → for •)for every step a → b, both b ↠ a• (ub) and a• ↠ b• (mon)Lemma (Z =⇒ strip =⇒ confluence)

Z

IWC, Tallinn, Estonia July 9th 2024

2

Z
Definition (Z-property of → for •)for every step a → b, both b ↠ a• (ub) and a• ↠ b• (mon)Lemma (Z =⇒ strip =⇒ confluence)

Z

IWC, Tallinn, Estonia July 9th 2024

2

Z
Definition (Z-property of → for •)for every step a → b, both b ↠ a• (ub) and a• ↠ b• (mon)Lemma (Z =⇒ strip =⇒ confluence)

Z
Z

IWC, Tallinn, Estonia July 9th 2024

2

Z
Definition (Z-property of → for •)for every step a → b, both b ↠ a• (ub) and a• ↠ b• (mon)Lemma (Z =⇒ strip =⇒ confluence)

strip

IWC, Tallinn, Estonia July 9th 20242

Z for λβTheorem (Loader 98)
for every step a →β b, both b ↠β a• (ub) and a• ↠β b• (mon), wherex•(λx.M)•((λx.M) N)•(M N)•

:=
:=
:=
:=

x

λx.M•
M• [x:=N• ]M• N•

IWC, Tallinn, Estonia July 9th 2024

otherwise (if M = x or M = P Q)

3

Z for λβTheorem (Loader 98)
for every step a →β b, both b ↠β a• (ub) and a• ↠β b• (mon), wherex•(λx.M)•((λx.M) N)•(M N)•

:=
:=
:=
:=

x

λx.M•
M• [x:=N• ]M• N•otherwise

Remarkfull development map • contracting all β -redex-patterns in λ-term(Church–Rosser 30s; Gross–Knuth, preprint 70s; Takahashi, Loader 90s)

IWC, Tallinn, Estonia July 9th 20243

Z for λβ proof
M

N
β
β

M•

N•
β

IWC, Tallinn, Estonia July 9th 2024

4

Z for λβ proofMNβupperboundM•N•
monotonic
Proof.
(ub) and (mon) by induction on M →β N

IWC, Tallinn, Estonia July 9th 2024

4

Z for λβ proof(λx.M) NβM[x:=N]
upperboundM•[x:=N•]
M[x:=N]•
monotonic
Proof.
(ub) and (mon) by induction on M →β N with base case β

IWC, Tallinn, Estonia July 9th 2024

4

Z for λβ proof(λx.M) N

M[x:=N]βextensive & term rewrite systemM•[x:=N•]
M[x:=N]•
right-hand side
Proof.
(ub) and (mon) by induction on M →β N with base case β , using:(extensive) M ↠β M•(ctx,sub) if M ↠β N and P ↠β Q, then M[x:=P] ↠β N[y:=Q](right-hand side) M• [x:=N• ] ↠β M[x:=N]•

IWC, Tallinn, Estonia July 9th 2024

4

Z for λβ proof(λx.M) N

M[x:=N]βextensive & term rewrite systemM•[x:=N•]
M[x:=N]•
right-hand side
Proof.
(ub) and (mon) by induction on M →β N with base case β , using:(extensive) M ↠β M•(ctx,sub) if M ↠β N and P ↠β Q, then M[x:=P] ↠β N[y:=Q](right-hand side) M• [x:=N• ] ↠β M[x:=N]•(ext),(rhs),(ctx) by induction on M; (sub) by induction on M →β N
IWC, Tallinn, Estonia July 9th 2024

4

Substitution lemma
Lemma (β -critical peak)((λx.M) N)[y:=Q] β ← (λy.(λx.M) N) Q →β (λy.M[x:=N]) Q is single-step joinable

IWC, Tallinn, Estonia July 9th 20245

Substitution lemma
Lemma (β -critical peak)((λx.M) N)[y:=Q] β ← (λy.(λx.M) N) Q →β (λy.M[x:=N]) Q is single-step joinable
Proof.

((λx.M) N)[y:=Q] = (λx.M[y:=Q]) N[y:=Q] →βM[y:=Q][x:=N[y:=Q]] =SL M[x:=N][y:=Q] β ← (λy.M[x:=N]) Q

IWC, Tallinn, Estonia July 9th 20245

Substitution lemma
Lemma (β -critical peak)((λx.M) N)[y:=Q] β ← (λy.(λx.M) N) Q →β (λy.M[x:=N]) Q is single-step joinable
Proof.

((λx.M) N)[y:=Q] = (λx.M[y:=Q]) N[y:=Q] →βM[y:=Q][x:=N[y:=Q]] =SL M[x:=N][y:=Q] β ← (λy.M[x:=N]) Q
Remarkclosure of →β under substitution (sub) ⇐⇒ β -critical peak lemma ⇐⇒ SL

IWC, Tallinn, Estonia July 9th 20245

Substitution lemma
Lemma (β -critical peak)((λx.M) N)[y:=Q] β ← (λy.(λx.M) N) Q →β (λy.M[x:=N]) Q is single-step joinable
Proof.

((λx.M) N)[y:=Q] = (λx.M[y:=Q]) N[y:=Q] →βM[y:=Q][x:=N[y:=Q]] =SL M[x:=N][y:=Q] β ← (λy.M[x:=N]) Q
Remarkclosure of →β under substitution (sub) ⇐⇒ β -critical peak lemma ⇐⇒ SL
proof of (rhs) uses substitution lemma

IWC, Tallinn, Estonia July 9th 20245

Substitution lemma
Lemma (β -critical peak)((λx.M) N)[y:=Q] β ← (λy.(λx.M) N) Q →β (λy.M[x:=N]) Q is single-step joinable
Proof.

((λx.M) N)[y:=Q] = (λx.M[y:=Q]) N[y:=Q] →βM[y:=Q][x:=N[y:=Q]] =SL M[x:=N][y:=Q] β ← (λy.M[x:=N]) Q
Remarkclosure of →β under substitution (sub) ⇐⇒ β -critical peak lemma ⇐⇒ SL
proof of (rhs) uses substitution lemma
β -redexes do have overlap (redex-patterns do not)

IWC, Tallinn, Estonia July 9th 20245

Substitution lemma
Lemma (β -critical peak)((λx.M) N)[y:=Q] β ← (λy.(λx.M) N) Q →β (λy.M[x:=N]) Q is single-step joinable
Proof.

((λx.M) N)[y:=Q] = (λx.M[y:=Q]) N[y:=Q] →βM[y:=Q][x:=N[y:=Q]] =SL M[x:=N][y:=Q] β ← (λy.M[x:=N]) Q
Remarkclosure of →β under substitution (sub) ⇐⇒ β -critical peak lemma ⇐⇒ SL
proof of (rhs) uses substitution lemma
β -redexes do have overlap; SL needed to have term rewrite system

IWC, Tallinn, Estonia July 9th 20245Formalisation of confluence by Z for λβ
Motivation
confluence of λβ -calculus PL-litmus test for proof assistants(inductive λ-terms and β -steps, binding, substitution, modulo α)

IWC, Tallinn, Estonia July 9th 2024

6

Formalisation of confluence by Z for λβ
Motivation
confluence of λβ -calculus PL-litmus test for proof assistants
claim: Z gives shortest proof of confluence of λβIWC, Tallinn, Estonia July 9th 2024

6

Formalisation of confluence by Z for λβ in Agda
Motivation
confluence of λβ -calculus PL-litmus test for proof assistants
claim: Z gives shortest proof of confluence of λβhere: test claim in Agda; had wanted to learn some Agda for some time
(done in 2021; learned at IWC 2023 of Andrea Laretto’s MSc thesis)

IWC, Tallinn, Estonia July 9th 2024

6

Formalisation of confluence by Z in Agda based on PLFA
Motivation
confluence of λβ -calculus PL-litmus test for proof assistants
claim: Z gives shortest proof of confluence of λβhere: test claim in Agda
design decision: adapt extant PLFA proof (by triangle property; Takahashi 95)(Programming Language Foundations in Agda by Wadler, Kokke, Siek 20
adaptation allowed reuse of inductive λ-terms, β -steps and SL
reuse good software engineering and useful since absolute Agda beginner)

IWC, Tallinn, Estonia July 9th 2024

6

Formalisation of confluence by Z in Agda based on PLFA
Motivation
confluence of λβ -calculus PL-litmus test for proof assistants
claim: Z gives shortest proof of confluence of λβhere: test claim in Agda
design decision: adapt extant PLFA proof (by triangle property
also means have to stick with design decisions of PLFA

IWC, Tallinn, Estonia July 9th 20246

λ-terms in PLFA
Definition (Nameless λ-term; de Bruijn 72)
PLFA design decision: scoped nameless λ-terms(avoids α-renaming at the expense of re-indexing)

IWC, Tallinn, Estonia July 9th 20247

λ-terms in PLFA
Definition (Nameless λ-term)
PLFA design decision: scoped nameless λ-terms

2: named λx.λy.x (x y), nameless λλS0 ((S0) 0), scoped 0 ⊢ λλS0 ((S0) 0)

IWC, Tallinn, Estonia July 9th 20247

λ-terms in PLFA
Definition (Nameless λ-term)
PLFA design decision: scoped nameless λ-terms
Definition (Scoped λ-term;& van der Looij & Zwitserlood 04??)i ⊢ t is nameless λ-term t in scope i(think of i as binding-stack with t closed within it; i is upperbound on indices in t)

IWC, Tallinn, Estonia July 9th 20247

λ-terms in PLFA
Definition (Nameless λ-term)
PLFA design decision: scoped nameless λ-terms
Definition (Scoped λ-term)i ⊢ t is nameless λ-term t in scope i (bottom–up) inductively derivable by:

IWC, Tallinn, Estonia July 9th 20247

λ-terms in PLFA
Definition (Nameless λ-term)
PLFA design decision: scoped nameless λ-terms
Definition (Scoped λ-term)i ⊢ t is nameless λ-term t in scope i

Remarkthese are generalised nameless λ-terms (Bird & Paterson 99; Hendriks &03)
PLFA only allows S on 0 and on other Ss; nameless λ-terms; no ho-signature

IWC, Tallinn, Estonia July 9th 20247

→β -steps in PLFA
Definition (Nameless β -reduction)
PLFA design decision: single substitution t [s] by parallel substitution 0 7→ s,Si 7→ i
(substitute s for the free 0s in t; decrement other indices)

IWC, Tallinn, Estonia July 9th 20248

→β -steps in PLFA
Definition (Nameless β -reduction)
PLFA design decision: single substitution t [s] by parallel substitution 0 7→ s,Si 7→ i→β on nameless λ-terms is compatible closure of β -scheme i ⊢ (λt) s = i ⊢ t[s]IWC, Tallinn, Estonia July 9th 20248

→β -steps in PLFA
Definition (Nameless β -reduction)
PLFA design decision: single substitution t [s] by parallel substitution 0 7→ s,Si 7→ i→β on nameless λ-terms is compatible closure of β -scheme i ⊢ (λt) s = i ⊢ t[s]0 ⊢ 2 2 →β 0 ⊢ (λS0 ((S0) 0))[2] = 0 ⊢ λS2 ((S2) 0) = 0 ⊢ λ2 (2 0)

IWC, Tallinn, Estonia July 9th 20248

→β -steps in PLFA
Definition (Nameless β -reduction)
PLFA design decision: single substitution t [s] by parallel substitution 0 7→ s,Si 7→ i→β on nameless λ-terms is compatible closure of β -scheme i ⊢ (λt) s = i ⊢ t[s]Lemma (λβ is a ho-term rewriting system; in PLFA)(ctx,sub) closure of reduction under contexts,substitutions(substitution lemma) for single substitution via parallel substitution

IWC, Tallinn, Estonia July 9th 20248

→β -steps in PLFA
Definition (Nameless β -reduction)
PLFA design decision: single substitution t [s] by parallel substitution 0 7→ s,Si 7→ i→β on nameless λ-terms is compatible closure of β -scheme i ⊢ (λt) s = i ⊢ t[s]Lemma (λβ is a ho-term rewriting system; in PLFA)(ctx,sub) closure of reduction under contexts,substitutions(substitution lemma) for single substitution via parallel substitution
Remark(ctx) is called congruence in PLFA (wrong; compatible)

IWC, Tallinn, Estonia July 9th 20248

→β -steps in PLFA
Definition (Nameless β -reduction)
PLFA design decision: single substitution t [s] by parallel substitution 0 7→ s,Si 7→ i→β on nameless λ-terms is compatible closure of β -scheme i ⊢ (λt) s = i ⊢ t[s]Lemma (λβ is a ho-term rewriting system; in PLFA)(ctx,sub) closure of reduction under contexts,substitutions(substitution lemma) for single substitution via parallel substitution
Remark(ctx) is called congruence in PLFA; (sub) missing from PLFA (50 loc)

IWC, Tallinn, Estonia July 9th 20248

→β -steps in PLFA
Definition (Nameless β -reduction)
PLFA design decision: single substitution t [s] by parallel substitution 0 7→ s,Si 7→ i→β on nameless λ-terms is compatible closure of β -scheme i ⊢ (λt) s = i ⊢ t[s]Lemma (λβ is a ho-term rewriting system; in PLFA)(ctx,sub) closure of reduction under contexts,substitutions(substitution lemma) for single substitution via parallel substitution
Remark(ctx) is called congruence in PLFA; (sub) missing from PLFA; (substitution lemma)
is called commutation in PLFA (wrong; self-distributivity / associativity)

IWC, Tallinn, Estonia July 9th 20248

→β -steps in PLFA
Definition (Nameless β -reduction)
PLFA design decision: single substitution t [s] by parallel substitution 0 7→ s,Si 7→ i→β on nameless λ-terms is compatible closure of β -scheme i ⊢ (λt) s = i ⊢ t[s]Lemma (λβ is a ho-term rewriting system; in PLFA)(ctx,sub) closure of reduction under contexts,substitutions(substitution lemma) for single substitution via parallel substitution
Remark(ctx) is called congruence in PLFA; (sub) missing from PLFA; (substitution lemma)
is called commutation in PLFA; terms / steps ad hoc (no signature)

IWC, Tallinn, Estonia July 9th 2024

8

Basic rewriting and full development map • for PLFA
app-cong : ∀{Γ } {K L M N : Γ ⊢ ⋆} → K —↠ L → M —↠ N → K · M —↠ L · N
rew-rew : ∀{Γ } {M N : Γ , ⋆ ⊢ ⋆ } {K L : Γ ⊢ ⋆ }→ M —↠ N→ K —↠ L------------→ M [ K ] —↠ N [ L ]Remark{. . .} indicates implicit argument; Γ is scope; ⋆ is singleton type of λ-terms
app-cong function taking reductions K ↠β L and K ↠β L yielding K M ↠β L N
rew-rew same but yielding closure under contexts,substitutions

IWC, Tallinn, Estonia July 9th 2024

9Basic rewriting and full development map • for PLFA
app-cong : ∀{Γ } {K L M N : Γ ⊢ ⋆} → K —↠ L → M —↠ N → K · M —↠ L · N
rew-rew : ∀{Γ } {M N : Γ , ⋆ ⊢ ⋆ } {K L : Γ ⊢ ⋆ }→ M —↠ N→ K —↠ L------------→ M [ K ] —↠ N [ L ]_• : ∀ {Γ A} → Γ ⊢ A → Γ ⊢ A(‘ x)• = ‘ x(λλ M)• = λλ (M •)((λλ M) · N)• = M • [ N • ](M · N)• = (M •) ·(N •)prime indicates index (as λ-term)

IWC, Tallinn, Estonia July 9th 20249(Extensive) M ↠ M• for PLFA
extensive : ∀ {Γ A} → (M : Γ ⊢ A) → M —↠ M •extensive (‘ _) = _ ■extensive (λλ M) = abs-cong (extensive M)
extensive ((λλ M) · N) = _ —→〈 β 〉 rew-rew (extensive M) (extensive N)
extensive (‘ _ · N) = appR-cong (extensive N)
extensive (L · M · N) = app-cong (extensive (L · M)) (extensive N)

IWC, Tallinn, Estonia July 9th 202410

(Extensive) M ↠ M• for PLFA
extensive : ∀ {Γ A} → (M : Γ ⊢ A) → M —↠ M •extensive (‘ _) = _ ■extensive (λλ M) = abs-cong (extensive M)
extensive ((λλ M) · N) = _ —→〈 β 〉 rew-rew (extensive M) (extensive N)
extensive (‘ _ · N) = appR-cong (extensive N)
extensive (L · M · N) = app-cong (extensive (L · M)) (extensive N)

Remarkrecursion on scoped nameless M : Γ ⊢ A (■ is empty reduction)otherwise only compatibility (wrongly named congruence in PLFA)

IWC, Tallinn, Estonia July 9th 2024

10

(Upperbound) N ↠ M• if M →β N for PLFA
upperbound : ∀ {Γ } → {M N : Γ ⊢ ⋆}→ M —→ N----→ N —↠ M •upperbound {_} {λλ _} (ζ ϕ) = abs-cong (upperbound ϕ)upperbound {_} {(‘ _) · _} {_} (ξ 2 ϕ) = appR-cong (upperbound ϕ)upperbound {_} {(λλ _) · M} {((λλ _) · M)} (ξ 1 (ζ ϕ)) = _ —→〈 β 〉 rew-rew (upperbound ϕ) (extensive M)
upperbound {_} {(λλ L) · _} {.((λλ L) · _)} (ξ 2 ϕ) = _ —→〈 β 〉 rew-rew (extensive L) (upperbound ϕ)upperbound {_} {(λλ L) · M} {.(subst (subst-zero M) L)} β = rew-rew (extensive L) (extensive M)
upperbound {_} {_ · _ · M} {.(_ · M)} (ξ 1 ϕ) = app-cong (upperbound ϕ) (extensive M)
upperbound {_} {K · L · _} {.(_ · _ · _)} (ξ 2 ϕ) = app-cong (extensive (K · L)) (upperbound ϕ)

IWC, Tallinn, Estonia July 9th 2024

11

(Upperbound) N ↠ M• if M →β N for PLFA
upperbound : ∀ {Γ } → {M N : Γ ⊢ ⋆}→ M —→ N----→ N —↠ M •upperbound {_} {λλ _} (ζ ϕ) = abs-cong (upperbound ϕ)upperbound {_} {(‘ _) · _} {_} (ξ 2 ϕ) = appR-cong (upperbound ϕ)upperbound {_} {(λλ _) · M} {((λλ _) · M)} (ξ 1 (ζ ϕ)) = _ —→〈 β 〉 rew-rew (upperbound ϕ) (extensive M)
upperbound {_} {(λλ L) · _} {.((λλ L) · _)} (ξ 2 ϕ) = _ —→〈 β 〉 rew-rew (extensive L) (upperbound ϕ)upperbound {_} {(λλ L) · M} {.(subst (subst-zero M) L)} β = rew-rew (extensive L) (extensive M)
upperbound {_} {_ · _ · M} {.(_ · M)} (ξ 1 ϕ) = app-cong (upperbound ϕ) (extensive M)
upperbound {_} {K · L · _} {.(_ · _ · _)} (ξ 2 ϕ) = app-cong (extensive (K · L)) (upperbound ϕ)

Remarkrecursion on M →β N (ζ ,ξ 1 ,ξ 2 traditional names of compatibility clauses)
otherwise only (extensive) and compatibility

IWC, Tallinn, Estonia July 9th 2024

11

•(Right-hand side) (M• )σ ↠ (Mσ )• for PLFA
rhss : ∀{Γ ∆} (M : Γ ⊢ ⋆) {σ τ : Subst Γ ∆} → ((x : Γ ∋ ⋆) → τ x ≡ σ x •)------------------→ subst τ (M •) —↠ (subst σ M)•
rhss (‘ x) eq rewrite (eq x) = _ ■rhss (λλ M) eq = abs-cong (rhss M (exts-bullet eq))
rhss ((‘ x) · M) {σ } eq rewrite (eq x) = —↠-trans(appR-cong (rhss M eq)) (app-bullet (σ x) (subst σ M)) where{- auxiliary rhs/monotonicity lemma for application -}app-bullet : ∀{Γ } (L M : Γ ⊢ ⋆) → L • · M • —↠ (L · M)•
app-bullet (‘ _) _ = _ ■app-bullet (λλ _) _ = (_ —→〈 β 〉 _ ■)app-bullet (_ · _) _ = _ ■rhss ((λλ L) · M) {τ = τ } eq rewrite (sym (subst-commute {N = L •} {M •} {τ })) =rew-rew (rhss L (exts-bullet eq)) (rhss M eq)
rhss (K · L · M) eq = app-cong (rhss (K · L) eq) (rhss M eq)

IWC, Tallinn, Estonia July 9th 2024

12•(Right-hand side) (M• )σ ↠ (Mσ )• for PLFA
rhss : ∀{Γ ∆} (M : Γ ⊢ ⋆) {σ τ : Subst Γ ∆} → ((x : Γ ∋ ⋆) → τ x ≡ σ x •)------------------→ subst τ (M •) —↠ (subst σ M)•
rhss (‘ x) eq rewrite (eq x) = _ ■rhss (λλ M) eq = abs-cong (rhss M (exts-bullet eq))
rhss ((‘ x) · M) {σ } eq rewrite (eq x) = —↠-trans(appR-cong (rhss M eq)) (app-bullet (σ x) (subst σ M)) where{- auxiliary rhs/monotonicity lemma for application -}app-bullet : ∀{Γ } (L M : Γ ⊢ ⋆) → L • · M • —↠ (L · M)•
app-bullet (‘ _) _ = _ ■app-bullet (λλ _) _ = (_ —→〈 β 〉 _ ■)app-bullet (_ · _) _ = _ ■rhss ((λλ L) · M) {τ = τ } eq rewrite (sym (subst-commute {N = L •} {M •} {τ })) =rew-rew (rhss L (exts-bullet eq)) (rhss M eq)
rhss (K · L · M) eq = app-cong (rhss (K · L) eq) (rhss M eq)

Remarkrecursion on scoped nameless M : Γ ⊢ ⋆ (σ, τ are parallel substitutions)

IWC, Tallinn, Estonia July 9th 202412

(Monotonic) M• ↠β N• if M →β N for PLFA
monotonic : ∀{Γ } → {M N : Γ ⊢ ⋆}→ M —→ N------→ M • —↠ N •monotonic (ζ ϕ) = abs-cong (monotonic ϕ)monotonic {_} {(‘ _) · _} {(‘ _) · _} (ξ 2 ϕ) = appR-cong (monotonic ϕ)monotonic {Γ } {(λλ M) · N} {.(subst (subst-zero N) M)} β = rhss M bullet-zero where{- bullet commutes with lifting terms to substitutions -}bullet-zero : (x : Γ , ⋆ ∋ ⋆) → subst-zero (N •) x ≡ subst-zero N x •bullet-zero Z = reflbullet-zero (S x) = reflmonotonic {_} {(λλ _) · _} {(λλ _) · _} (ξ 1 (ζ ϕ)) = rew-rew (monotonic ϕ) (_ ■)monotonic {_} {(λλ M) · _} {.((λλ M) · _)} (ξ 2 ϕ) = rew-rew (M • ■) (monotonic ϕ)monotonic {_} {_ · _ · _} {(λλ _) · _} (ξ 1 ϕ) = —↠-trans (appL-cong (monotonic ϕ)) (_ —→〈 β 〉 _ ■)monotonic {_} {_ · _ · _} {(‘ _) · _} (ξ 1 ϕ) = appL-cong (monotonic ϕ)monotonic {_} {_ · _ · _} {_ · _ · _} (ξ 1 ϕ) = appL-cong (monotonic ϕ)monotonic {_} {_ · _ · _} {_ · _ · _} (ξ 2 ϕ) = appR-cong (monotonic ϕ)

IWC, Tallinn, Estonia July 9th 2024

13

Conclusions• 4 key properties 65 loc
induction on scoped nameless λ-term(extensive)=⇒

induction on derivations(upperbound)(right-hand side)=⇒(monotonic)• nameless = uninamed; scopes are stacks (Hendriks &03; not lists)• basic term rewrite theory of λβ in PLFA is incomplete(no signature; does not show it’s a ho-term rewrite system, no sub)• section on confluence of λβ in PLFA is suboptimal(shorter proof via Z; the notes attributing are incorrect / improper)

IWC, Tallinn, Estonia July 9th 2024

14

Future work
Questions• single proof instantiating to full development,full superdevelopment maps?

Remarkfull superdevelopment map • contracting β -redex-patterns in inside–out sweep
00s)(Aczel 80s; van Raamsdonk 90s, Dehornoy &IWC, Tallinn, Estonia July 9th 2024

15

Future work
Questions• single proof instantiating to full development,full superdevelopment maps?
if a →β b then b ↠β a• ↠β b• (Z; Dehornoy &x•(λx.M)•(M N)•

:=
:=
:=
:=

08), where

x

λx.M•
M′ [x:=N• ]if M• = λx.M′

M• N•otherwise

IWC, Tallinn, Estonia July 9th 2024

15

Future work
Questions• single proof instantiating to full development,full superdevelopment maps?
• avoid duplicates of substitution lemmata in PLFA? (for reindexing)

IWC, Tallinn, Estonia July 9th 2024

15

Future work
Questions• single proof instantiating to full development,full superdevelopment maps?
• avoid duplicates of substitution lemmata in PLFA?
by working with generalised scoped λ-terms (instead of separate indices)

Remarkgeneralised scoped λ-terms due to Bird & Paterson 99, Hendriks &der Looij & Zwitserlood 04

IWC, Tallinn, Estonia July 9th 2024

02 & van

15

Future work
Questions• single proof instantiating to full development,full superdevelopment maps?
• avoid duplicates of substitution lemmata in PLFA?
• avoid parallel substitution in PLFA? (only single substitution)

IWC, Tallinn, Estonia July 9th 2024

15

Future work
Questions• single proof instantiating to full development,full superdevelopment maps?
• avoid duplicates of substitution lemmata in PLFA?
• avoid parallel substitution in PLFA?
by working with single substitution at a given depth

Remarkanalogous to Huet’s 94 Coq formalisation (based on 6 axioms); cf. proceedings

IWC, Tallinn, Estonia July 9th 2024

15

Future work
Questions• single proof instantiating to full development,full superdevelopment maps?
• avoid duplicates of substitution lemmata in PLFA?
• avoid parallel substitution in PLFA?
• avoid maximal scope extrusion? (work with minimal scope extrusion)
Remarkanalogous to Hendriks &IWC, Tallinn, Estonia July 9th 2024

03; cf. paper in proceedings

15

Future work
Questions• single proof instantiating to full development,full superdevelopment maps?
• avoid duplicates of substitution lemmata in PLFA?
• avoid parallel substitution in PLFA?
• avoid maximal scope extrusion?
Thanks to
Patrick Dehornoy, Christian Sternagel, Julian Nagele, Bertram Felgenhauer for Z
Andrea Laretto 24 for discussing confluence by Z in Agda (for PLFA; ongoing)

IWC, Tallinn, Estonia July 9th 202415