Verifications and uses with zippers

From The Twelf Project
Jump to: navigation, search
This is Literate Twelf
Code: here
Status: %% OK %%
Output: here.

In the verifications and uses article we saw a typical presentation of a logic of verifications and uses, and in article on hereditary substitution with zippers we saw an attempt to clean up the "ugly part" of that proof by defining a zipper-like structure over terms. The reason that global soundness for this system did not hold is that Twelf could not verify (without the use of a structural metric) that a "zipped" use was the same size as an "unzipped" use, so termination checking failed when a recursive call was made on a term that had been unzipped.

In this article, we give a different solution. This system has something of the flavor of a spine form presentation; however, as we discussed in the hereditary substitution with zippers, it is still much closer to a natural deduction system - the analogue of the natural deduction term atm (⊃E (⊃E (⊃E (var x) N1) N2) N3) in the natural deduction system is atm x (⊃E (⊃E (⊃E end N1) N2) N3) in this version of "natural deduction" - the form of proofs stays the same with the exception that the head variable x has been pulled out into the front.

Propositions and rules

prop : type.
atom : type.
%block bl_atom : block {qp : atom}.

a : atom -> prop.
⊃ : prop -> prop -> prop. %infix right 9 ⊃.
∧ : prop -> prop -> prop. %infix right 8 ∧.

hyp   : prop -> type.
verif : prop -> type.
use   : prop -> prop -> type.
%block bl_hyp : some {A : prop} block {x : hyp A}.

end : use A A.
atm : hyp A -> use A (a Q) -> verif (a Q).
⊃I  : (hyp A -> verif B) -> verif (A ⊃ B).
⊃E  : use A (B₁ ⊃ B₂) -> verif B₁ -> use A B₂.
∧I  : verif A₁ -> verif A₂ -> verif (A₁ ∧ A₂).
∧E₁ : use A (B₁ ∧ B₂) -> use A B₁.
∧E₂ : use A (B₁ ∧ B₂) -> use A B₂.

Global completeness

Because we have changed the logic, the η-expansion theorem has changed somewhat. Recall that, in the pure system of verifications and uses, the statement of global completeness/η-expansion was that, for all A, we can verify the truth of A in any context where we can use the fact that A is true. In this system, however, we don't ever use A in a vacuum - we always take a hypothesis of B and then prove that, given B, we can use A. The eta expansion theorem reflects this: it says that, for any A, given an arbitrary B that we have hypothesized to be true and a proof that we can use A given B, we can prove A.

The structure of the η-expansion theorem's proof is then mostly unchanged from the system of verifications and uses. 

eta : {A} ({B} hyp B -> use B A -> verif A) -> type.
%mode eta +A -B.

- : eta (a Q) ([B][x][r] atm x r).
- : eta (A₁ ⊃ A₂) ([B][x][r] ⊃I [y] N₂ B x (⊃E r (N₁ A₁ y end)))
     <- eta A₁ ([B] N₁ B : hyp B -> use B A₁ -> verif A₁)
     <- eta A₂ ([B] N₂ B : hyp B -> use B A₂ -> verif A₂).
- : eta (A₁ ∧ A₂) ([B][x][r] ∧I (N₁ B x (∧E₁ r)) (N₂ B x (∧E₂ r)))
     <- eta A₁ ([B] N₁ B : hyp B -> use B A₁ -> verif A₁)
     <- eta A₂ ([B] N₂ B : hyp B -> use B A₂ -> verif A₂).

%worlds (bl_atom | bl_hyp) (eta _ _).
%total A (eta A _).

Let's see some examples of η-expansions: 

%solve _ : {q1}{q2}{q3} eta (a q1 ⊃ a q2 ⊃ a q3) (X q1 q2 q3).
Twelf 1.7.1+ (r1896, built 05/05/15 at 12:56:43 on yazoo.plparty.org)

%solve 
{q1:atom} {q2:atom} {q3:atom}
   eta (a q1 ⊃ a q2 ⊃ a q3)
      ([B:prop] [x:hyp B] [x1:use B (a q1 ⊃ a q2 ⊃ a q3)] X q1 q2 q3 B x x1).
 OK
_ :
   {q1:atom} {q2:atom} {q3:atom}
      eta (a q1 ⊃ a q2 ⊃ a q3)
         ([B:prop] [x:hyp B] [x1:use B (a q1 ⊃ a q2 ⊃ a q3)]
             ⊃I
                ([y:hyp (a q1)]
                    ⊃I
                       ([y1:hyp (a q2)]
                           atm x (⊃E (⊃E x1 (atm y end)) (atm y1 end)))))
   = [q1:atom] [q2:atom] [q3:atom] %-% (%-% %-% %-%) %-%.


%% OK %%
%solve _ : {q1}{q2}{q3} eta ((a q1 ⊃ a q2) ⊃ a q3) (X q1 q2 q3).
Twelf 1.7.1+ (r1896, built 05/05/15 at 12:56:43 on yazoo.plparty.org)

%solve 
{q1:atom} {q2:atom} {q3:atom}
   eta ((a q1 ⊃ a q2) ⊃ a q3)
      ([B:prop] [x:hyp B] [x1:use B ((a q1 ⊃ a q2) ⊃ a q3)]
          X q1 q2 q3 B x x1).
 OK
_ :
   {q1:atom} {q2:atom} {q3:atom}
      eta ((a q1 ⊃ a q2) ⊃ a q3)
         ([B:prop] [x:hyp B] [x1:use B ((a q1 ⊃ a q2) ⊃ a q3)]
             ⊃I
                ([y:hyp (a q1 ⊃ a q2)]
                    atm x
                       (⊃E x1
                           (⊃I ([y1:hyp (a q1)] atm y (⊃E end (atm y1 end)))))))
   = [q1:atom] [q2:atom] [q3:atom] %-% %-% (%-% %-% %-%).


%% OK %%

Global soundness

The real benefit of this modified natural deduction system is that we no longer need to take any detours to prove the hereditary substitution theorem: when we reach the atm case where we must verify an atomic proposition by using a proof of its truth, we know exactly what hypothesis we are using. If the hypothesis is the one we're substituting for, then we call out to the hsubst_rn theorem where we do repeated reductions, and if the hypothesis is not, we call out to the hsubst_rr theorem where the structure of the use stays essentially the same. 

hsubst_n  : {A}    verif A -> (hyp A -> verif B) -> verif B -> type.
hsubst_rr : {A}    verif A -> (hyp A -> use C B) -> use C B -> type.
hsubst_rn : {A}{B} verif A -> (hyp A -> use A B) -> verif B -> type.
%mode hsubst_n  +A    +M₀ +M -N.
%mode hsubst_rr +A    +M₀ +R -R'.
%mode hsubst_rn +A +B +M₀ +R -N.

- : 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) (N y : verif B₂).
- : hsubst_n A M₀ ([x] ∧I (M₁ x) (M₂ x)) (∧I N₁ N₂)
     <- hsubst_n A M₀ ([x] M₁ x) (N₁ : verif B₁)
     <- hsubst_n A M₀ ([x] M₂ x) (N₂ : verif B₂).
- : hsubst_n A M₀ ([x] atm x (R x)) N
     <- hsubst_rn A (a Q) M₀ ([x] R x) N.
- : hsubst_n A M₀ ([x] atm Y (R x)) (atm Y R')
     <- hsubst_rr A M₀ ([x] R x) R'.

- : hsubst_rr A M₀ ([x] ⊃E (R x) (M x)) (⊃E R' N)
     <- hsubst_rr A M₀ ([x] R x) R' 
     <- hsubst_n A M₀ ([x] M x) N.
- : hsubst_rr A M₀ ([x] ∧E₁ (R x)) (∧E₁ R')
     <- hsubst_rr A M₀ ([x] R x) R'.
- : hsubst_rr A M₀ ([x] ∧E₂ (R x)) (∧E₂ R')
     <- hsubst_rr A M₀ ([x] R x) R'.
- : hsubst_rr A M₀ ([x] end) end.

- : hsubst_rn A B₂ M₀ ([x] ⊃E (R x) (M x)) N'
     <- hsubst_rn A (B₁ ⊃ B₂) M₀ ([x] R x) ((⊃I [y] N y) : verif (B₁ ⊃ B₂))
     <- hsubst_n A M₀ ([x] M x) (M' : verif B₁)
     <- hsubst_n B₁ M' ([y] N y) (N' : verif B₂).
- : hsubst_rn A B₁ M₀ ([x] ∧E₁ (R x)) N₁
     <- hsubst_rn A (B₁ ∧ B₂) M₀ ([x] R x) (∧I N₁ N₂ : verif (B₁ ∧ B₂)).
- : hsubst_rn A B₂ M₀ ([x] ∧E₂ (R x)) N₂
     <- hsubst_rn A _ M₀ ([x] R x) (∧I N₁ N₂ : verif (B₁ ∧ B₂)).
- : hsubst_rn A A M₀ ([x] end) M₀.

%worlds (bl_atom | bl_hyp)
(hsubst_n _ _ _ _)
(hsubst_rr _ _ _ _) 
(hsubst_rn _ _ _ _ _).

%reduces B <= A (hsubst_rn A B _ _ _).

%total {(A B C) (M R S)}
(hsubst_n A _ M _)
(hsubst_rr B _ R _) 
(hsubst_rn C _ _ S _).


Retrieved from "http://twelf.org/w/index.php?title=Verifications_and_uses_with_zippers&oldid=6160"