Overview of FTY support for pseudo-terms.

The book "clause-processors/pseudo-term-fty" defines a fixing function and convenient accessors and constructors for fty-discipline support for pseudo-terms. It also provides macros that generate appropriate theorems about evaluators allowing them to understand the new accessors and constructors.

We treat the pseudo-term type as a sum of five kinds of products:

:null , encompassing the unique pseudo-termNIL as well as (ill-formed) non-symbol atoms and calls with non-symbol atom function names; has no field:var , encompassing non-nil symbols; field:name :quote , conses whose car isquote ; field:val fncall , conses whose car is a non-quote symbol; fields:fn andargs lambda , conses whose car is a cons; fields:formals ,body , andargs .

Each of these product kinds has a constructor that uses the typical naming
convention; e.g., to make a lambda, use

(b* (((pseudo-lambda x))) (list x.formals x.body x.args))

An alternative constructor

The

The macro pseudo-term-case can be used to conveniently branch on the kind of term and access the fields; see its documentation for examples.

The macro def-ev-pseudo-term-fty-support admits several theorems about an evaluator, enabling reasoning about evaluation over the provided constructors and accessors. See its documentation for details.

Another macro, def-ev-pseudo-term-congruence, admits only a subset of the theorems produced by def-ev-pseudo-term-fty-support, proving a pseudo-term-equiv congruence for the evaluator but no rules pertaining to the FTY-style accessors and updaters.

- Pseudo-term-lambda
- Constructor for a lambda call (
:lambda ) pseudo-term. - Pseudo-term-call
- Constructor that produces either a function call or lambda call pseudo-term, depending whether the given function is a function symbol or lambda.
- Pseudo-term-fncall
- Constructor for function call (
:fncall ) pseudo-terms. - Pseudo-lambda
- Type of, and constructor for, a lambda function, used in the FTY support for pseudo-terms.
- Pseudo-term-var
- Constructor for variable (
:var ) pseudo-terms. - Pseudo-term-quote
- Constructor for :quote pseudo-terms.
- Pseudo-term-kind
- Return the kind of a pseudo-term input (a keyword symbol).
- Pseudo-term-null
- Constructor for null pseudo-terms. Just returns NIL.
- Pseudo-fnsym
- Type of a function symbol used in the FTY support for pseudo-terms.
- Pseudo-term-case
- Case macro for pseudo-term objects.
- Pseudo-term-count
- Measure for recursion over pseudo-terms
- Def-ev-pseudo-term-fty-support
- Admit theorems about an evaluator that allow reasoning about FTY-style accessors and constructors for pseudo-terms.
- Def-ev-pseudo-term-congruence
- Prove that pseudo-term-fix is transparent to an evaluator and
that the evaluator thus has a
pseudo-term-equiv congruence on its first argument. - Pseudo-term-fix
- Fixing function for pseudo-terms that supports FTY-style discipline and is transparent to evaluators.
- Pseudo-var
- Type of a variable symbol used in the FTY support for pseudo-terms.
- Pseudo-term-list-fix
- Fixing function for pseudo-term lists that supports FTY-style discipline and is transparent to evaluators.
- Pseudo-fn
- Type of a function (either symbol or lambda), used in pseudo-term FTY support.