Every term in HOL can be summarised by the BNF term ::= var | const | term @ term | \v. term
where @ is function application (and if you use concrete syntax, you don’t write the @), and \v. term represents a lambda-abstraction. If you want to programmatically generate terms, using this view is probably best, particularly if you use the standard API calls that help with common cases. There is a surface syntax that users write, but it’s extensible (users can define new infixes, new binders and perhaps new mix-fixes and the like). That makes it impossible/hard to generate a grammar for everything that the pretty-printer might generate. On the other hand, the parser will almost certainly let you input using the core syntax in such a way that you don’t need to worry about the pretty versions. Thus, you can write !x. p x ==> q x Or (!) (\x. (==>) (p x) (q x)) where I’ve had to put parentheses around the ! and the ==> to stop the parser from getting confused by the fact that they are also infixes/binders. There are also other issues to do with distinguishing variables from constants, and from getting the types of these things to be what you want. Michael From: "Miranda, Brando" <miran...@illinois.edu> Date: Saturday, 9 November 2019 at 02:50 To: hol-info <hol-info@lists.sourceforge.net> Subject: [Hol-info] grammar for HOL Light terms Hi, This is my first message to the HOL list so hope its not out of the rules for the list (couldn’t find the rules). I wanted to find the formal grammar for generating terms (formulas) in HOL (Light). I was wondering were I could find such a specification? Thanks! Brando
_______________________________________________ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
