locally nameless Takahashi translation

Stream: computer science

[Chris Henson]

I am trying to translate this proof from PLFA into cslib. I've seen this called the Takahashi translation elsewhere, but have not been able to find a project that uses it alongside a locally nameless representation, has anyone else?

I've been working in this branch and it's probably easier to work from there is you want to look at this, but here's also an extracted mwe of where I got stuck (the two sorry in takahashi_triangle):

import Mathlib

universe u

variable {Var : Type u} [DecidableEq Var]

inductive Term (Var : Type u)
| bvar : ℕ → Term Var
| fvar : Var → Term Var
| abs  : Term Var → Term Var
| app  : Term Var → Term Var → Term Var

namespace Term

/-- Variable opening of the ith bound variable. -/
def openRec (i : ℕ) (sub : Term Var) : Term Var → Term Var
| bvar i' => if i = i' then sub else bvar i'
| fvar x  => fvar x
| app l r => app (openRec i sub l) (openRec i sub r)
| abs M   => abs <| openRec (i+1) sub M

scoped notation:68 e "⟦" i " ↝ " sub "⟧"=> Term.openRec i sub e

/-- Variable opening of the closest binding. -/
def open' {X} (e u):= @Term.openRec X 0 u e

scoped infixr:80 " ^ " => Term.open'

inductive Parallel : Term Var → Term Var → Prop
| fvar (x : Var) : Parallel (fvar x) (fvar x)
| app : Parallel L L' → Parallel M M' → Parallel (app L M) (app L' M')
| abs (xs : Finset Var) :
    (∀ x ∉ xs, Parallel (m ^ fvar x) (m' ^ fvar x)) → Parallel (abs m) (abs m')
| beta (xs : Finset Var) :
    (∀ x ∉ xs, Parallel (m ^ fvar x) (m' ^ fvar x) ) →
    Parallel n n' →
    Parallel (app (abs m) n) (m' ^ n')

scoped notation3 t:39 " ⭢ₚ " t':39 => Parallel t t'

-- this is proven, but leaving out of the mwe since it has many dependencies
lemma para_open_out (L : Finset Var) (mem : ∀ x, x ∉ L → (M ^ fvar x) ⭢ₚ N ^ fvar x)
    (para : M' ⭢ₚ N') : (M ^ M') ⭢ₚ (N ^ N') := sorry

def takahashi : Term Var → Term Var
| bvar x => bvar x
| fvar i => fvar i
| abs M => abs M.takahashi
| app (abs N) M => N.takahashi ^ M.takahashi
| app L R => app L.takahashi R.takahashi

theorem takahashi_triangle (M N : Term Var) (para : M ⭢ₚ N) : N ⭢ₚ M.takahashi := by
  induction para
  case fvar => constructor
  case abs L _ _ =>
    refine Parallel.abs L ?_
    sorry
  case beta L _ _ _ np =>
    refine para_open_out L ?_ np
    sorry
  case app L' _ _ _ L_L' _ Lt Rt =>
    induction L'
    case abs =>
      cases L_L'
      cases Lt
      next xs _ => exact Parallel.beta xs (by aesop) Rt
    all_goals constructor <;> aesop

abbrev Diamond (R : α → α → Prop) := ∀ {A B C : α}, R A B → R A C → (∃ D, R B D ∧ R C D)

theorem triangle_diamond {f : α → α} (tri : ∀ (A B), R A B → R B (f A)) : Diamond R := by
  intros A B C AB AC
  exact ⟨f A, tri _ _ AB, tri _ _ AC⟩

theorem para_diamond : Diamond (@Parallel Var) := triangle_diamond takahashi_triangle

[Fabrizio Montesi]

Assuming the property about takahashi and open works, this fixes the abs case.

---@[simp]
---theorem takahashi_open {M : Term Var} : (M ^ fvar x).takahashi = M.takahashi ^ fvar x := by
---  exact takahashi_openRec
+@[simp]
+theorem takahashi_open {M : Term Var} : (M ^ fvar x).takahashi = M.takahashi ^ fvar x := by
+ exact takahashi_openRec

 theorem takahashi_triangle (M N : Term Var) (para : M ⭢ₚ N) : N ⭢ₚ M.takahashi := by
   induction para
   case fvar => aesop
-  case abs L q w =>
+  case abs M N L q w =>
     refine Parallel.abs L ?_
-    sorry
-  case beta L _ _ _ np =>
+    intro x hx
+    specialize q x hx
+    have ih := takahashi_triangle _ _ q
+    rw [takahashi_open] at ih
+    exact ih

[Fabrizio Montesi]

I tried making a PR but I've been stupid with my git-fu... luckily the patch is short.

[Chris Henson]

Ahh I left a comment there, but should have mentioned before posting. I realized this, but the theorem takahashi_openRec is not true without some side conditions. Consider:

-- fvar "y"
#eval (app (bvar 1).abs (fvar "x")).takahashi⟦1 ↝ fvar "y"⟧

-- bvar 1
#eval (app (bvar 1).abs (fvar "x"))⟦1 ↝ fvar "y"⟧.takahashi

I couldn't figure out is being locally closed was sufficient, that's why it was commented out.

[Fabrizio Montesi]

Right. I don't know if that's sufficient, but a good sign is that Takahashi preserves LC (or at least it would be.. I haven't checked. Does it?).

[Chris Henson]

It should, since it is only making beta reductions. I'll try prove it once I'm back at a computer.