Confluence of minimal φ-calculus

This file contains a formalization of minimal φ-calculus and the proof of its confluence.

References

• Nikolai Kudasov and Violetta Sim. 2023. Formalizing 𝜑-Calculus: A Purely Object-Oriented Calculus of Decorated Objects.
• Jean L. Krivine. 1993. Lambda-Calculus, Types and Models. Ellis Horwood, USA.

Defition of minimal φ-calculus terms

@[reducible]

def Attr : Type

Equations

• Attr = String

inductive Term : Type

• loc : Nat → Term
• dot : Term → Attr → Term
• app : Term → Attr → Term → Term
• obj {lst : List Attr} : Record (Option Term) lst → Term

@[reducible]

def Bindings (lst : List String) : Type

Equations

• Bindings lst = Record (Option Term) lst

Defition of increment, substitution, its properties, and auxiliary definitions that involve terms

def incLocatorsFrom (n : Nat) (term : Term) : Term

Locator increment [KS22, Definition 2.5]

Equations

• incLocatorsFrom n (Term.loc m) = if m < n then Term.loc m else Term.loc (m + 1)
• incLocatorsFrom n (t.dot a) = (incLocatorsFrom n t).dot a
• incLocatorsFrom n (t.app a u) = (incLocatorsFrom n t).app a (incLocatorsFrom n u)
• incLocatorsFrom n (Term.obj o) = Term.obj (incLocatorsFromLst (n + 1) o)

def incLocatorsFromLst (n : Nat) {lst : List Attr} (bnds : Bindings lst) : Bindings lst

Equations

• incLocatorsFromLst n Record.nil = Record.nil
• incLocatorsFromLst n (Record.cons a not_in none tail) = Record.cons a not_in none (incLocatorsFromLst n tail)
• incLocatorsFromLst n (Record.cons a not_in (some term) tail) = Record.cons a not_in (some (incLocatorsFrom n term)) (incLocatorsFromLst n tail)

def incLocators : Term → Term

Equations

• incLocators = incLocatorsFrom 0

def substitute : Nat × Term → Term → Term

Locator substitution [KS22, Fig. 1]

Equations

• substitute (k, v) (Term.loc m) = if m < k then Term.loc m else if (m == k) = true then v else Term.loc (m - 1)
• substitute (k, v) (t.dot a) = (substitute (k, v) t).dot a
• substitute (k, v) (t.app a u) = (substitute (k, v) t).app a (substitute (k, v) u)
• substitute (k, v) (Term.obj o) = Term.obj (substituteLst (k + 1, incLocators v) o)

def substituteLst {lst : List Attr} : Nat × Term → Bindings lst → Bindings lst

Equations

• substituteLst (k, v) Record.nil = Record.nil
• substituteLst (k, v) (Record.cons a not_in none tail) = Record.cons a not_in none (substituteLst (k, v) tail)
• substituteLst (k, v) (Record.cons a not_in (some term) tail) = Record.cons a not_in (some (substitute (k, v) term)) (substituteLst (k, v) tail)

instance instMinOptionNat_minimal : Min (Option Nat)

Equations

• One or more equations did not get rendered due to their size.

@[irreducible]

def min_free_loc (zeroth_level : Nat) : Term → Option Nat

Minimal free locator in a term, if free locators exist, assuming free locators start at zeroth_level.

Equations

• min_free_loc zeroth_level (Term.loc m) = if m < zeroth_level then none else some (m - zeroth_level)
• min_free_loc zeroth_level (t.dot a) = min_free_loc zeroth_level t
• min_free_loc zeroth_level (t.app a u) = min (min_free_loc zeroth_level t) (min_free_loc zeroth_level u)
• min_free_loc zeroth_level (Term.obj Record.nil) = none
• min_free_loc zeroth_level (Term.obj (Record.cons key a none tail)) = min_free_loc zeroth_level (Term.obj tail)
• min_free_loc zeroth_level (Term.obj (Record.cons key a (some t) tail)) = min (min_free_loc (zeroth_level + 1) t) (min_free_loc zeroth_level (Term.obj tail))

def le_nat_option_nat : Nat → Option Nat → Prop

Equations

• le_nat_option_nat x✝ (some k) = (x✝ ≤ k)
• le_nat_option_nat x✝ none = True

theorem le_min_option {j : Nat} {option_n1 option_n2 : Option Nat} (le_min : le_nat_option_nat j (min option_n1 option_n2)) : le_nat_option_nat j option_n1 ∧ le_nat_option_nat j option_n2

theorem le_min_option_reverse {j : Nat} {option_n1 option_n2 : Option Nat} (le_and : le_nat_option_nat j option_n1 ∧ le_nat_option_nat j option_n2) : le_nat_option_nat j (min option_n1 option_n2)

theorem min_free_loc_inc {i j : Nat} {v : Term} (free_locs_v : le_nat_option_nat i (min_free_loc j v)) : le_nat_option_nat (i + 1) (min_free_loc j (incLocatorsFrom j v))

IncLocatorsFrom increments minimal free locator if it acts only on free locators.

theorem min_free_loc_inc.traverse_bindings {i j : Nat} {lst : List Attr} (bindings : Bindings lst) (free_locs : le_nat_option_nat i (min_free_loc j (Term.obj bindings))) : le_nat_option_nat (i + 1) (min_free_loc j (Term.obj (incLocatorsFromLst (j + 1) bindings)))

@[irreducible]

theorem subst_inc_cancel (v u : Term) (j k i zeroth_level : Nat) (le_ji : j ≤ i + zeroth_level) (le_ki : k ≤ i + zeroth_level) (le_0j : zeroth_level ≤ j) (le_0k : zeroth_level ≤ k) (v_loc : le_nat_option_nat i (min_free_loc zeroth_level v)) : v = substitute (j, u) (incLocatorsFrom k v)

substitute and incLocatorsFrom cancel effect of each other, if they act only on free locators.

@[irreducible]

theorem subst_inc_cancel_Lst {lst : List Attr} (bindings : Bindings lst) (u : Term) (j k i zeroth_level : Nat) (le_ji : j ≤ i + zeroth_level) (le_ki : k ≤ i + zeroth_level) (le_0j : zeroth_level ≤ j) (le_0k : zeroth_level ≤ k) (v_loc : le_nat_option_nat i (min_free_loc zeroth_level (Term.obj bindings))) : bindings = substituteLst (j + 1, incLocators u) (incLocatorsFromLst (k + 1) bindings)

def lookup {lst : List Attr} (l : Bindings lst) (a : Attr) : Option (Option Term)

Equations

• lookup Record.nil a = none
• lookup (Record.cons name a_1 opAttr tail) a = if (name == a) = true then some opAttr else lookup tail a

theorem lookup_none_not_in {lst : List Attr} {l : Bindings lst} {a : Attr} (lookup_none : lookup l a = none) : ¬a ∈ lst

theorem lookup_none_preserve {lst : List Attr} {l1 : Bindings lst} {a : Attr} (lookup_none : lookup l1 a = none) (l2 : Bindings lst) : lookup l2 a = none

def insert_φ {lst : List Attr} (l : Bindings lst) (a : Attr) (u : Option Term) : Bindings lst

Equations

• insert_φ Record.nil a u = Record.nil
• insert_φ (Record.cons name a_1 opAttr tail) a u = if (name == a) = true then Record.cons name a_1 u tail else Record.cons name a_1 opAttr (insert_φ tail a u)

inductive IsAttached {lst : List Attr} : Attr → Term → Bindings lst → Type

• zeroth_attached {lst : List Attr} (a : Attr) (not_in : ¬a ∈ lst) (t : Term) (l : Bindings lst) : IsAttached a t (Record.cons a not_in (some t) l)
• next_attached {lst : List Attr} (a : Attr) (t : Term) (l : Bindings lst) (b : Attr) : a ≠ b → (not_in : ¬b ∈ lst) → (u : Option Term) → IsAttached a t l → IsAttached a t (Record.cons b not_in u l)

theorem isAttachedIsIn {lst : List Attr} {a : Attr} {t : Term} {l : Bindings lst} : ∀ (a✝ : IsAttached a t l), a ∈ lst

theorem Insert.insertAttachedStep {a b : Attr} {neq : a ≠ b} {t : Term} {lst : List Attr} {not_in : ¬b ∈ lst} {u : Option Term} {l : Bindings lst} : insert_φ (Record.cons b not_in u l) a (some t) = Record.cons b not_in u (insert_φ l a (some t))

theorem Insert.insertAttached {a : Attr} {t : Term} {lst : List Attr} {l : Bindings lst} : ∀ (a✝ : IsAttached a t l), insert_φ l a (some t) = l

theorem Insert.insertTwice {lst : List Attr} (l : Bindings lst) (a : Attr) (t t' : Term) : insert_φ (insert_φ l a (some t')) a (some t) = insert_φ l a (some t)

def Insert.insert_new_isAttached {lst : List Attr} {l : Bindings lst} {a : Attr} {t t' : Term} : IsAttached a t l → IsAttached a t' (insert_φ l a (some t'))

Equations

• One or more equations did not get rendered due to their size.
• Insert.insert_new_isAttached (IsAttached.zeroth_attached a not_in t l_2) = ⋯.mpr (IsAttached.zeroth_attached a not_in t' l_2)

Substitution Lemma

theorem inc_swap (i j : Nat) (le_ij : i ≤ j) (t : Term) : incLocatorsFrom i (incLocatorsFrom j t) = incLocatorsFrom (j + 1) (incLocatorsFrom i t)

Increment swap [KS22, Lemma A.9]

theorem inc_swap_Lst (i j : Nat) (le_ij : i ≤ j) {lst : List Attr} (o : Bindings lst) : incLocatorsFromLst (i + 1) (incLocatorsFromLst (j + 1) o) = incLocatorsFromLst (j + 1 + 1) (incLocatorsFromLst (i + 1) o)

theorem subst_inc_swap (i j : Nat) (le_ji : j ≤ i) (t u : Term) : substitute (i + 1, incLocatorsFrom j u) (incLocatorsFrom j t) = incLocatorsFrom j (substitute (i, u) t)

Increment and substitution swap [KS22, Lemma A.8]

theorem subst_inc_swap_Lst (i j : Nat) (le_ji : j ≤ i) {lst : List Attr} (o : Bindings lst) (u : Term) : substituteLst (i + 1 + 1, incLocators (incLocatorsFrom j u)) (incLocatorsFromLst (j + 1) o) = incLocatorsFromLst (j + 1) (substituteLst (i + 1, incLocators u) o)

theorem inc_subst_swap (i j : Nat) (le_ji : j ≤ i) (t u : Term) : incLocatorsFrom i (substitute (j, u) t) = substitute (j, incLocatorsFrom i u) (incLocatorsFrom (i + 1) t)

Increment and substitution swap, dual to A.8

theorem inc_subst_swap_Lst (i j : Nat) (le_ji : j ≤ i) {lst : List Attr} (o : Bindings lst) (u : Term) : incLocatorsFromLst (i + 1) (substituteLst (j + 1, incLocators u) o) = substituteLst (j + 1, incLocators (incLocatorsFrom i u)) (incLocatorsFromLst (i + 1 + 1) o)

theorem subst_swap (i j : Nat) (le_ji : j ≤ i) (t u v : Term) (free_locs_v : le_nat_option_nat i (min_free_loc 0 v)) : substitute (i, v) (substitute (j, u) t) = substitute (j, substitute (i, v) u) (substitute (i + 1, incLocators v) t)

Substitutions swap [KS22, Lemma A.7]

theorem subst_swap_Lst (i j : Nat) (le_ji : j ≤ i) {lst : List Attr} (o : Bindings lst) (u v : Term) (free_locs_v : le_nat_option_nat i (min_free_loc 0 v)) : substituteLst (i + 1, incLocators v) (substituteLst (j + 1, incLocators u) o) = substituteLst (j + 1, incLocators (substitute (i, v) u)) (substituteLst (i + 1 + 1, incLocators (incLocators v)) o)

theorem lookup_inc_attached (t : Term) (i : Nat) (c : Attr) {lst : List Attr} (l : Bindings lst) (lookup_eq : lookup l c = some (some t)) : lookup (incLocatorsFromLst i l) c = some (some (incLocatorsFrom i t))

theorem lookup_inc_void (i : Nat) (c : Attr) {lst : List Attr} (l : Bindings lst) (lookup_eq : lookup l c = some none) : lookup (incLocatorsFromLst i l) c = some none

theorem lookup_inc_none (i : Nat) (c : Attr) {lst : List Attr} (l : Bindings lst) (lookup_eq : lookup l c = none) : lookup (incLocatorsFromLst i l) c = none

theorem inc_insert {i : Nat} {c : Attr} {lst : List Attr} {l : Bindings lst} {v : Term} : insert_φ (incLocatorsFromLst (i + 1) l) c (some (incLocators (incLocatorsFrom i v))) = incLocatorsFromLst (i + 1) (insert_φ l c (some (incLocators v)))

theorem lookup_subst_attached (t : Term) {u : Term} (i : Nat) (c : Attr) {lst : List Attr} (l : Bindings lst) (lookup_eq : lookup l c = some (some t)) : lookup (substituteLst (i, u) l) c = some (some (substitute (i, u) t))

theorem lookup_subst_void {u : Term} (i : Nat) (c : Attr) {lst : List Attr} (l : Bindings lst) (lookup_eq : lookup l c = some none) : lookup (substituteLst (i, u) l) c = some none

theorem lookup_subst_none {u : Term} (i : Nat) (c : Attr) {lst : List Attr} (l : Bindings lst) (lookup_eq : lookup l c = none) : lookup (substituteLst (i, u) l) c = none

theorem subst_insert {i : Nat} {c : Attr} {lst : List Attr} {l : Bindings lst} {u v : Term} : insert_φ (substituteLst (i + 1, incLocators u) l) c (some (incLocators (substitute (i, u) v))) = substituteLst (i + 1, incLocators u) (insert_φ l c (some (incLocators v)))