Eval on variables

[laskowsp]

Hello Dr. Farmer,

I met with Dr. Carette today, who said that the way to implement Eval to work on variables is to have it include an environment parameter, which maps variables to terms, and should throw an exception if the variable is undefined in the environment.

Could you provide any input on whether or not this method is the best way to go about implementing Eval?

[wmfarmer]

No, this is not how eval should be implemented. It is just a term constructor like quote, comb, etc. As I mentioned before, it has two arguments. The first is a term of type epsilon, and the second is a type. The type of an eval term is the same as its second argument.

eval does not need an environment parameter because the values of variables are determined by the context in which an eval term is employed. eval would need the environment parameter if it were a function.

Besides eval, you need to also implement is-free-in as an HOL function and IS-EFFECTIVE-IN as an OCaml function (see the paper for details). After these are in place with their related lemmas, the next two steps will be to (1) specify the properties of eval (see Axiom B10 in the paper) and (2) develop a version of substitution for terms that contain eval (which we will have to discuss).

[JacquesCarette]

Oops, sorry! I keep thinking 'functionally', an PL, not 'logic without beta reduction'.

[laskowsp]

I see, thank you.

[laskowsp]

Do you have any suggestions on how to go about implementing IS-EFFECTIVE-IN as an OCaml function? It seems like one of those things that should be defined in the logic, because there's all sorts of cases that it could potentially have to cover and therefore seems like it should be up to the user to prove.

E.g. if I have a constant function f:num->num that takes a number and always returns 3, then presumably x:num would not be effective in f(x), but there's no easy way to check for this through OCaml since it would require adding some sort of way to automatically simplify terms, and then there would need to be some reasoning mechanism to detect this constant function.

[wmfarmer]

IS-EFFECTIVE-IN is defined as a notational definition in the paper on p. 21. It takes a variable x_alpha and a term B_beta and returns a formula of the form

forsome y_alpha . ((lambda x_alpha . B_beta) y_alpha not= B_beta)

where y_alpha is not the same variable as x_alpha. So all IS-EFFECTIVE-IN has to do is to build this term.

[laskowsp]

Alright, thanks!

[wmfarmer]

Patrick, at Monday's meeting I would like for you to give Jacques and me an overview of the code you have added to HOL Light (if that works). I have a few questions about the code.

[JacquesCarette]

Reminder: I am away for 2 weeks, starting tomorrow morning. Back to Mac on Monday 24th.

[wmfarmer]

OK, Patrick, since Jacques is away let just you and I will meet on Monday at 9:30 to discuss your code.

[laskowsp]

Yes, that works. Is there any specific features you'd like me to focus on in the overview or should I just give a brief demonstration of everything that's been added?

On Thu, Jul 6, 2017 at 4:30 PM, wmfarmer notifications@github.com wrote:

OK, Patrick, since Jacques is away let just you and I will meet on Monday at 9:30 to discuss your code.

— You are receiving this because you authored the thread. Reply to this email directly, view it on GitHub https://github.com/JacquesCarette/hol-light/issues/10#issuecomment-313510637, or mute the thread https://github.com/notifications/unsubscribe-auth/AbN_2VP0IQl-SinKwnymAY1oudf5RFSSks5sLUPygaJpZM4ONhoE .

[wmfarmer]

An overview would be best with the opportunity for me to ask lots of questions.

[laskowsp]

Okay, I've also noticed a symbol I'm not used to seeing in the definition of some of the logical formulas inside the paper. Table 3 defines it as (lambda) x. (lambda) y. x = (x /\ y), which seems to be the definition of implication, would this be correct? Is there any difference between this operator and the ==> operator?

I've attached a screenshot just in case this is an issue with the way my laptop is displaying the paper.

[wmfarmer]

This symbol indeed denotes implication. It is often used by logicians. I like using it so that the arrows --> and ==> can be used for other things.

[laskowsp]

I see, thank you. Will all of these properties have to be defined as axioms inside HOL, or should some of them be provable?

[wmfarmer]

All of these will have to be defined as axioms. A good test will be to prove the Syntactic Law of Disquotation (Theorem 6.6.1) from these axioms.