Issue with epsilon variables in syntactic law of disquotation proof

[laskowsp]

I am trying to prove the syntactic law of disquotation starting from how it is done in the paper - a case split over all possible types of epsilon. This works for QuoConst and QuoVar, but as soon as it gets to something more complicated like App, I run into the following issue.

val it : goalstack = 1 subgoal (3 total)

  0 [`x = App a0 a1`]

`(eval (x) to (A)) = CTT x`

There is no restriction that a0 must be a QuoConst of type A->B, and I have not yet been able to find any way to enforce this restriction. Since the type is unknown to HOL, I am unable to prove isExpr, and can't use the axioms to continue with the proof.

What would be the best way to resolve this problem?

[JacquesCarette]

You need some predicate that tells you that a quote is 'well formed' (proper?). There are lots of things of type epsilon which are junk, such as an App a0 a1 with a0 not of the right type.

Your well-formedness predicate needs to tell you exactly what you need to make the proof of disquotation go through.

[I am sure there is such a predicate in Bill's paper, I just forget its name; and the law of disquotation either implicitly assumes well-formedness, or implicitly assumes the host logic supports undefinedness.]

[laskowsp]

I see, I believe isExpr is this predicate. The issue is that the axioms of evaluation are of the form isExpr A ==> B, so I cannot use them without proving that a0 is well-formed, but I also cannot prove a0 is well-formed in all cases because epsilon does allow junk terms.

[wmfarmer]

What is your statement of the law of disquotation? It should be [[ "A_alpha"]] = A_alpha. The construction that equals "A_alpha" must thus be proper. So you are missing something. Perhaps you need to prove the lemma

isExpr (termToConstruction "A_alpha") alpha

[laskowsp]

My statement for the law of disquotation is (eval (x:epsilon) to A) = (CTT x):A where CTT is just an internal use of the ConstructionToTerm function that will take something of type epsilon like QuoVar "x" (TyBase "num") and return an HOL term, in this case, x:num.

I think proving that lemma would help, though isExpr is defined in terms of isValidType, which checks against a list of known types, so I feel like a similar issue will arise here.

[wmfarmer]

This is not the correct statement of the law of disquotation since x could denote an improper construction. The correction statement should be something like

eval (quote A alpha) to alpha = A

[laskowsp]

I see - this should work, however, quote does not take a type, and HOL types and epsilon types are currently incompatible with each other. In fact, I don't think it's possible for Eval to be able to accept both formats, because HOL types are defined as their own seperate type called hol_type, while types of the type type are defined as an HOL term.

How would I go about saying that A is of type alpha under these conditions?

[laskowsp]

I just realized I may be interpreting this incorrectly - is quote meant to be Q_ _Q or the function inside epsilon? If it's the former, would eval Q_ H_ A:alpha _H _Q to alpha = A work?

Edit: Holed terms need to be of type epsilon, so it seems it would not. Since variable substitution does not work in quotes, it's not possible to just write Q_ A:alpha _Q.

[wmfarmer]

quote is meant to be the new constructor Quote in the inductive type of terms:

type term = private Var of string hol_type | Const of string hol_type | Comb of term term | Abs of term term | Quote of term hol_type | Hole of term hol_type | Eval of term * hol_type

Are you representing Quote in the user syntax as Q_ ... _Q?

[laskowsp]

Yes, it is represented as Q_ ... _Q, e.g. Quote(x + 3,:num) would be input as Q_ x + 3 _Q.

[wmfarmer]

Good. So the answer to your question whether

eval Q H A:alpha _H _Q to alpha = A

would work is yes.

[laskowsp]

I think I may have misunderstood something about holes - I thought they were only supposed to accept terms of type epsilon? If so, A:alpha cannot be accepted by a hole because it can turn out to be of any type.

[wmfarmer]

I misread your question; I didn't notice the H_ and _H. The correct form of the law of disquotation should be

eval (Q_ A:alpha _Q) to alpha = A

[laskowsp]

Okay, the problem with this though is that variable substitution is disabled for quotations, and this is what is used for instantiating into theorems, so HOL will not interpret A:alpha as a placeholder for any expression, but the syntax of the term A:alpha.

[wmfarmer]

You are thus saying that there is not a mechanism in HOL to prove schemas. I need to look at the five axioms for evaluation. What file are they in?

[wmfarmer]

We can talk a bit about this at the BBQ this afternoon.

[laskowsp]

Apologies for the late reply, I took my lunch at 1:30. The axioms for evaluation are located in AdditionalFunctions.ml:

let app_split = new_axiom `((isExprType At (TyBiCons "fun" (a:type) (b:type)) /\ (isExprType Bt a)) ==> ((eval (app At Bt) to B) = ((eval At to A->B) (eval Bt to A))))`;;
let quotable = new_axiom `(isExprType e (TyBase "epsilon")) ==> ((eval (quo e) to epsilon) = e)`;; 
let abs_split = new_axiom `isExprType C (TyVar "B") /\ ~(isFreeIn (QuoVar x t) (Quo C)) ==> (eval (e_abs (QuoVar x t) C) to (A->B)) = (\x. (eval (C) to (B))):A->B`;;
let var_disquo = new_axiom `(eval (QuoVar a b) to A) = (CTT (QuoVar a b)):A`;;
let cons_disquo = new_axiom `(eval (QuoConst a b) to A) = (CTT (QuoConst a b)):A`;;

Regarding the substitution problem, would it be possible to add something like holes to mark certain variables as able to be instantiated into?

[laskowsp]

@wmfarmer

I'm still unable to see the list you mentioned yesterday, could you please post it again? Thanks!

[wmfarmer]

Sorry, I must have forgot to hit the Comment button.

Here is the list:

1. Create a rule of inference that expresses the Law of Quotation (Theorem 6.4.1).
2. Create five rules of inference that express the five properties of evaluation (Axiom B10).
3. Modify the substitution procedure so that it stops when evals are met (I will have to help you out with this).
4. Create rules of inference that express Axioms B11, B12, and B13. These rules will be used where substitution stops due to an eval.
5. State and prove a construction version of the law of disquotation. (It will not be possible to prove the law of disquotation directly in HOL Light since it is a schema.)

[wmfarmer]

You should take a look at the HOL Light rules of inference given in

 http://www.cl.cam.ac.uk/~jrh13/papers/hollight.pdf

to get an idea of what rules of inference look like logically.

[laskowsp]

Thank you for the resource, I notice that these rules are all defined inside HOL's kernel as OCaml functions, which is how I've been going about implementing the rules of inference, so I feel like I'm on the right track.

[wmfarmer]

Yes, they are defined in the metalogic (using OCaml). The problem we ran into is that schemas evidently can only be defined in the metalogic and not in the logic itself (i.e., inside HOL).

[laskowsp]

Hello Dr. Farmer, If I understand correctly, both you and Dr. Carette are away this week, so does that mean there will be no meeting today?

[JacquesCarette]

Correct.