I am working with HOL-Light parser and keeping seeing references to preterm parser.

What is a preterm parser?

The most informative statement I find is from the HOL-Light reference for the parse_pretype function.

This is mostly an internal function; pretypes and preterms are used as an intermediate representation for typechecking and overload resolution and are not normally of concern to users.


1 Answer 1


Since HOL Light is based on $\lambda$ Calculus and HOL Light is typed and as we know there is untyped $\lambda$ Calculus and typed $\lambda$ Calculus, HOL Light starts by parsing something close to untyped $\lambda$ Calculus, creating pre-terms. Then it applies a typing checking and typing phase, along with resolving overloaded operators resulting is something closer to typed $\lambda$ Calculus. Obviously HOL is much more than typed $\lambda$ Calculus, but the point here is to understand what pre-term means with regards to parsing.

The only reference I have found for this is in

Lectures on the Curry-Howard Isomorphism
Section 1.2 Pre-terms and $\lambda$-terms.

Specifically how this is done in HOL Light is in the parser module:

The pre-terms are created with

let ptm = (parse_pteterm << lex << explode) input

and the type checking, etc. is done with

let term = (term_of_preterm << (retypecheck [])) ptm

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge that you have read and understand our privacy policy and code of conduct.

Not the answer you're looking for? Browse other questions tagged or ask your own question.