JacquesCarette / hol-light-qe

The HOL Light theorem prover (moved from Google code)
Other
7 stars 1 forks source link

Specification of functions for Epsilon #2

Closed laskowsp closed 7 years ago

laskowsp commented 7 years ago

I would like to confirm that I am understanding what each of the functions laid out in Dr. Farmer's paper should accomplish, as I am slightly confused as to what some of them should do. Would it be possible to confirm that the definitions below are correct and correct any that are not?

is-var: Given anything in type epsilon, returns boolean true if the given item is of type QuoVar, otherwise returns false is-var-alpha: Same as is-var, but also takes a type, returns boolean true if the given item is a QuoVar of type alpha, else false.

is-cons/is-cons-alpha: Function exactly the same as is-var/is-var-alpha respectively, but with QuoConsts instead of QuoVars

app: Given two items e1 and e2 both of type epsilon, returns (App e1 e2) abs: Given two items e1 and e2 both of type epsilon, returns (Abs e1 e2)

quo: Takes a type epsilon and applies the quotation operation - essentially a quotation operator restricted to type epsilon?

is-expr: This is the main one I am confused about - is it checking that an expression is eval-free? If so, what would this look like considering we have yet to define an Eval operator inside epsilon? is-expr-alpha: Same as is-expr but checks that the expression's type is that of alpha as well

The second last one that looks like a [ : Also confused by this one - the paper says it's true if the first expression is a valid sub-expression of the second - what is meant by valid sub-expression here? Is it simply checking that e1 is located somewhere inside e2, or is it checking that the expression makes sense as well? (e.g. false if an attempt is made to apply constant "5" to constant "3" for example)

is-free-in: If the first expression (has to be a variable) appears free anywhere inside the second, return true

Thank you!

wmfarmer commented 7 years ago

Patrick, I will be on campus this afternoon. Are you free at 2:30? If so, we can discuss your questions then.

laskowsp commented 7 years ago

Yes, I am free at 2:30.

JacquesCarette commented 7 years ago

So has this been resolved? It is good to close issues when they are no longer active. Or to add some updates. This helps document the state of things -- and also makes it easier to recall when comes the time to write a paper.