isConstruction implementation

[laskowsp]

I spoke with Dr. Farmer this morning about an operation called isConstruction that would verify that an epsilon term construction represents a quoted term. The example I was shown where to apply this would be when using quasi quotation to substitute into a quotation.

Are there any other scenarios where an epsilon construction would fail isConstruction? If not, would it be easier to implement quasi quotation first and then add this check?

Edit: Also - what would be the best way to go about implementing quasi quotation? I'm thinking another addition to HOL's term definitions may be necessary, since these are a separate class of variables and would not really fit in to Var. The other idea I have come up with is a special constructed type for Vars to "mark" them but this seems like a messier solution.

[JacquesCarette]

How accurate is isConstruction supposed to be? Some constructions might fail because (for example) you are applying a boolean to another boolean [since epsilon is untyped]. So what is isConstruction really for? It might make sense to have several is* routines that verify different things (and might build one upon another).

In other words, as I don't know what invariants isConstruction is supposed to verify, I can't really tell you about the failures you'll encounter!

You can implement quasiquotes first or second, I think both are feasible. Note that quasiquotes don't just involve variables -- you need to have 'holes' more generally. What have you read on quoting? There are two operators (quote and splice, or ` and , in Lisp, or ...) that make up quasiquotes.

[laskowsp]

I have not looked into how Lisp handles quasiquotation at all, I think reading up on this would be a good idea. Do you have any recommended resources?

I've already got a definition in the epsilon type isExpr that verifies that a term is well formed, applying a boolean to another boolean would cause this check to fail. My understanding is that isConstruction should check that a term construction can be turned back into an application of quotation to a particular term. That is, it should satisfy isExpr but include some additional checks.

For instance, QuoConst "T" (TyBase "bool") would pass this check because it can be converted to Q_ T _Q, but something like applying the /\\ operator to a "hole" of type bool would not work, because although it is valid in terms of types, it is not representative of an actual term until that hole is filled in.

[JacquesCarette]

Some of the standard terminology comes from Scheme. You can read a short intro http://courses.cs.washington.edu/courses/cse341/04wi/lectures/14-scheme-quote.html

It's also worth reading the same from the Racket perspective (section 4.10 and 4.11 of the manual) https://docs.racket-lang.org/guide/quote.html

From an ML perspective, you can read https://www.cs.rice.edu/~taha/publications/journal/dspg04a.pdf but some of the techniques in there are out-dated (i.e. section 1 is great, 2 is ok, and 3 is not how people would do this now).

[laskowsp]

Thank you, I think I'm starting to understand.

So what quasi quotation should look like is the ability to essentially "interrupt" the parsing of a quotation, evaluate some value that is being unquoted, and use the result of that evaluation in place of the unquoted expression?

[JacquesCarette]

Yes. Assume that what you evaluate gives something of type epsilon.

[laskowsp]

Alright, the problem I'm seeing here is that HOL is entirely static. That is, if I input 2 + 3, I get 2 + 3, not 5, how would I actually simplify the value being unquoted?

Or would it be better to define unquote as a function that checks if the term inside it can be simplified, and if so, puts the resultant term inside the quote, otherwise throwing an exception, therefore relying on the user to perform the simplification?

[JacquesCarette]

I don't know! This is indeed tricky. Are there really no 'functions' in HOL that beta-reduce "automatically" ?

[laskowsp]

From what I've seen, they are extremely spread out, arithmetic on natural numbers alone has at least five conversion functions to attempt, not to mention that there are a lot of definitions such as "HD" for lists and even the functions defined in the epsilon type that need to be passed to REWRITE_CONV to be used.

Edit: It appears that passing [ARITH;ALL] to REWRITE_CONV makes it perform simple arithmetic and boolean logic, but it is still incapable of working some things on it's own automatically such as (x = 5) ==> ((x = 5) \/ (x = 2)), which should evaluate to true.

[laskowsp]

One more question: in Lisp it is not possible to unquote undefined variables:

`(1 ,(+ x 3))

*** - EVAL: variable X has no value

Should we replicate this behavior, or would unquote (2 * x - x) result in x being quoted?

[JacquesCarette]

I think you should meet with Bill to discuss this. It's tricky!

[laskowsp]

I agree, I'll email Dr. Farmer and ask him to meet.

[wmfarmer]

Patrick, let's meet this afternoon about 1:30. I will contact you later after lunch with the exact time.

[laskowsp]

Alright, thank you.

[wmfarmer]

I am in my office now. So please drop by whenever you are ready.

[laskowsp]

I can come by now, I'm on my way.