Hereditary substitution with a zipper

This article represents a (partially unsuccessful) attempt to remove the “ugly” portion from the global soundness proof in the verifications and uses article. The language of propositions and rules (and, as a result, the argument for global completeness) is unchanged from the verifications and uses, and so we omit it here.

This article is an intermediate point between the verifications and uses article and the verifications and uses with zippers article. | hidden = true

%sort prop %.
%sort atom %.
%block bl_atom {qp atom}%.
%term a %pi atom %-> prop %.
%term ⊃ %pi prop %-> prop %-> prop %.
%prec %right 9 ⊃ %.
%term ∧ %pi prop %-> prop %-> prop %.
%prec %right 8 ∧ %.
%sort hyp {_ prop} %.
%sort verif {_ prop} %.
%sort use {_ prop} %.
%block bl_hyp [A prop] {x hyp A}%.
%term var %pi (hyp A) %-> (use A) %.
%term atm %pi (use (a Q)) %-> (verif (a Q)) %.
%term ⊃I %pi (%pi (hyp A) %-> (verif B)) %-> (verif (A ⊃ B)) %.
%term ⊃E %pi (use (A ⊃ B)) %-> (verif A) %-> (use B) %.
%term ∧I %pi (verif A) %-> (verif B) %-> (verif (A ∧ B)) %.
%term ∧E₁ %pi (use (A ∧ B)) %-> (use A) %.
%term ∧E₂ %pi (use (A ∧ B)) %-> (use B) %.

Rather than the (somewhat ugly) process used to find the main variable in the verifications and uses example, in this example we will create a sort-of zipper data structure that allows us to “pull out” the head variable from the inside of a term.

Defining pseudo-zippers

A zipper data structure is a way of describing paths into complex structures. A “real” zipper over an atomic term has the structure of a spine in a spine form presentation of logic; what we present here isn’t “really” a spine (or a zipper).

%sort zip {_ prop} {_ prop} %.
%term end zip A A %.
%term ⊃Z %pi (zip A (B₁ ⊃ B₂)) %-> (verif B₁) %-> (zip A B₂) %.
%term ∧Z₁ %pi (zip A (B₁ ∧ B₂)) %-> (zip A B₁) %.
%term ∧Z₂ %pi (zip A (B₁ ∧ B₂)) %-> (zip A B₂) %.
%sort use' {_ prop} %.
%term · %pi (hyp A) %-> (zip A B) %-> (use' B) %.
%prec %none 10 · %.

For instance, the use' corresponding to (⊃E (⊃E (⊃E (var x) $N_{1}$) $N_{2}$) $N_{3}$) is x · (⊃Z (⊃Z (⊃Z end $N_{1}$) $N_{2}$) $N_{3}$) --- the head variable x has been brought out to the top of the term, but the subterm $N_{1}$ is still nested more deeply than the subterms $N_{2}$ and $N_{3}$. In a conversion to spine form, we would not only expose the head variable x but would make $N_{1}$ the “least deeply nested” subterm and make $N_{3}$“ the “most deeply nested” subterm.

Zipping and unzipping

We need to both show that we can zip and unzip a use into a use', and vice versa. These two proofs are essentially the same logic program run in opposite directions, but STELF only allows us to assign a single mode to a metatheorem, so rather than just copying and pasted we have “cleaned up” both the unzip and rezip functions a bit.

%sort unzip {_ use B} {_ use' B} %.
%term _ %pi (unzip (⊃E R N) (X · ⊃Z Z N)) %<- (unzip R (X · Z)) %.
%term _ %pi (unzip (∧E₁ R) (X · ∧Z₁ Z)) %<- (unzip R (X · Z)) %.
%term _ %pi (unzip (∧E₂ R) (X · ∧Z₂ Z)) %<- (unzip R (X · Z)) %.
%term _ unzip (var X) (X · end) %.
%mode unzip %in %out %.
%worlds (bl_atom bl_hyp) (unzip _ _) %.
%total R (unzip R _) %.
%sort rezip {_ hyp A} {_ zip A B} {_ use B} %.
%term _ %pi (rezip X (⊃Z Z N) (⊃E R N)) %<- (rezip X Z R) %.
%term _ %pi (rezip X (∧Z₁ Z) (∧E₁ R)) %<- (rezip X Z R) %.
%term _ %pi (rezip X (∧Z₂ Z) (∧E₂ R)) %<- (rezip X Z R) %.
%term _ rezip X end (var X) %.
%mode rezip %in %in %out %.
%worlds (bl_atom bl_hyp) (rezip _ _ _) %.
%total Z (rezip _ Z _) %.

Global soundness

%sort hsubst_n {A} {_ verif A} {_ %pi (hyp A) %-> (verif B)} {_ verif B} %.
%sort hsubst_r {A} {_ verif A} {_ %pi (hyp A) %-> (use' (a Q))} {_ verif (a Q)} %.
%sort hsubst_rr {A} {_ verif A} {_ %pi (hyp A) %-> (zip C B)} {_ zip C B'} %.
%sort hsubst_rn {A} {B} {_ verif A} {_ %pi (hyp A) %-> (zip A B)} {_ verif B} %.
%mode hsubst_n %in %in %in %out %.
%mode hsubst_r %in %in %in %out %.
%mode hsubst_rr %in %in %in %out %.
%mode hsubst_rn %in %in %in %in %out %.
%term _
  %pi (hsubst_n A M₀ ([x] ⊃I ([y] M x y)) (⊃I ([y] N y)))
  %<- ({y hyp B₁} hsubst_n A M₀ ([x] M x y) (%the (verif B₂) (N y))) %.
%term _
  %pi (hsubst_n A M₀ ([x] ∧I (M₁ x) (M₂ x)) (∧I N₁ N₂))
  %<- (hsubst_n A M₀ ([x] M₁ x) (%the (verif B₁) N₁))
  %<- (hsubst_n A M₀ ([x] M₂ x) (%the (verif B₂) N₂)) %.
%term _
  %pi (hsubst_n A M₀ ([x] atm (R x)) N)
  %<- ({x hyp A} unzip (R x) (R' x))
  %<- (hsubst_r A M₀ ([x] R' x) N) %.
%term _ %pi (hsubst_r A M₀ ([x] x · Z x) N) %<- (hsubst_rn A _ M₀ ([x] Z x) N) %.
%term _
  %pi (hsubst_r A M₀ ([x] Y · Z x) (atm R))
  %<- (hsubst_rr A M₀ ([x] Z x) Z')
  %<- (rezip Y Z' R) %.
%term _
  %pi (hsubst_rr A M₀ ([x] ⊃Z (Z x) (M x)) (⊃Z Z' N))
  %<- (hsubst_rr A M₀ ([x] Z x) Z')
  %<- (hsubst_n A M₀ ([x] M x) N) %.
%term _ %pi (hsubst_rr A M₀ ([x] ∧Z₁ (Z x)) (∧Z₁ Z')) %<- (hsubst_rr A M₀ ([x] Z x) Z') %.
%term _ %pi (hsubst_rr A M₀ ([x] ∧Z₂ (Z x)) (∧Z₂ Z')) %<- (hsubst_rr A M₀ ([x] Z x) Z') %.
%term _ hsubst_rr A M₀ ([x] end) end %.
%term _
  %pi (hsubst_rn A _ M₀ ([x] ⊃Z (Z x) (M x)) N')
  %<- (hsubst_rn A _ M₀ ([x] Z x) (%the (verif (B₁ ⊃ B₂)) (⊃I ([y] N y))))
  %<- (hsubst_n A M₀ ([x] M x) (%the (verif B₁) M'))
  %<- (hsubst_n B₁ M' ([y] N y) (%the (verif B₂) N')) %.
%term _
  %pi (hsubst_rn A _ M₀ ([x] ∧Z₁ (Z x)) N₁)
  %<- (hsubst_rn A _ M₀ ([x] Z x) (%the (verif (B₁ ∧ B₂)) (∧I N₁ N₂))) %.
%term _
  %pi (hsubst_rn A _ M₀ ([x] ∧Z₂ (Z x)) N₂)
  %<- (hsubst_rn A _ M₀ ([x] Z x) (%the (verif (B₁ ∧ B₂)) (∧I N₁ N₂))) %.
%term _ hsubst_rn A _ M₀ ([x] end) M₀ %.
%worlds (bl_atom bl_hyp) (hsubst_n _ _ _ _) (hsubst_rr _ _ _ _) (hsubst_rn _ _ _ _ _) (hsubst_r _ _ _ _) %.
%reduces <= B A (hsubst_rn A B _ _ _) %.

Failure of termination checking

The fact that our representation uses both proofs use A and proofs use' A means that we will run afowl of STELF’s termination checker --- an unzipped term has a different size than the corresponding zipped term. We could certainly convince STELF that zipping and unzipping preserved size by using the same tree-like structural metric used in the concrete representation case study, but that would be notationally heavy and unenlightening.

Another option is to ask STELF to trust us:

%reduces = R' R (unzip R R') %.