4v-sexprs
S-Expression representation of four-valued expressions.
We represent expressions in our four-valued logic using a simple
S-Expression (sexpr) format.
The semantics of these expressions is given by 4v-sexpr-eval.
Loosely speaking,
- NIL is special and always evaluates to X.
- All atoms other than NIL represent variables and get their values from
an environment.
- (f a1 a2 ... an) is a function application of f to arguments
a1 ... an, where each ai is itself a sexpr.
Since we only have four constants, we don't permit quoted constants; instead
we just have constant functions. That is, in any environment,
- (T) produces T,
- (F) produces F,
- (Z) produces Z, and
- (X) produces X.
We also have around a dozen functions like AND, OR, NOT,
ITE, etc., that correspond to the 4v-operations. The particular
set of understood functions are determined by 4v-sexpr-eval.
A wonderful feature of our 4v sexpr language is that, since all of these
operations are monotonic,
monotonicity is an intrinsic property of every sexpr.
As with our aig and ubdd
representations, we generally expect to create all sexprs with hons, and
we often memoize operations that deal with sexprs. We provide some
4vs-constructors for building s-expressions.
Subtopics
- 4v-sexpr-vars
- Collect the set of variables in an s-expression.
- 4v-sexpr-eval
- Evaluate a sexpr under an environment.
- 4v-sexpr-to-faig
- Translation from 4v-sexprs into a faigs.
- 4v-sexpr-restrict-with-rw
- 4v-sexpr-restrict with inline rewriting.
- 4vs-constructors
- Primitive functions for constructing 4v-sexprs.
- 4v-sexpr-compose-with-rw
- 4v-sexpr-compose with inline rewriting.
- 4v-sexpr-restrict
- Basic substitution operation for 4v-sexprs.
- 4v-sexpr-alist-extract
- Extract a portion of a 4v-sexpr alist.
- 4v-sexpr-compose
- Alternate substitution operation for 4v-sexprs.
- 4v-nsexpr-p
- (4v-nsexpr-p x) recognizes s-expressions where every variable
is a natural number.
- 4v-sexpr-purebool-p
- Does a 4v-sexpr always evaluate to a purely Boolean value, i.e., is
it never X or Z?
- 4v-sexpr-<=
- Extension of the four-valued lattice ordering to sexprs.
- Sfaig
- A simplified version of 4v-sexpr-to-faig that constructs its
own onoff list out of the variables of the sexpr.
- Sexpr-equivs
- Useful equivalence relations for reasoning about 4v-sexprs.
- 3v-syntax-sexprp
- Recognizer for 4v-sexprs that cannot evaluate to Z.
- Sexpr-rewriting
- 4v-sexpr-ind
- Basic structural induction scheme for s-expressions.
- 4v-alist-extract
- Gather up a sub-alist from some 4v environment.
