Semantics-shallowly-embedded
Shallowly embedded semantics of PFCSes.
The semantics informally described in semantics
can be formalized in a shallowly embedded way,
by defining ACL2 functions that turn expressions and constraints
into ACL2 terms and functions that express the semantics.
In the names of the ACL2 functions defined below,
the prefix sesem stands for `shallowly embedded semantics'.
Subtopics
- Name-list-to-symbol-list
- Turn a list of PFCS relation or variable names
into a list of ACL2 symbols.
- Name-to-symbol
- Turn a PFCS relation or variable name into an ACL2 symbol.
- Sesem-definition
- Shallowly embedded semantics of a definition.
- Sesem-expression
- Shallowly embedded semantics of expressions.
- Sesem-constraint
- Shallowly embedded semantics of a constraint.
- Sesem-gen-fep-terms
- Generate a list of terms (fep x1 p), ..., (fep xn p)
from a list of variables x1, ..., xn.
- Sesem-expression-list
- Shallowly embedded semantics of lists of expressions.
- Sesem-definition-list
- Shallowly embedded semanics of a list of definitions.
- Sesem-constraint-list
- Shallowly embedded semantics of a list of constraints.
- Name-set-to-symbol-list
- Lift name-to-symbol to a mapping
from sets of strings to lists of symbols.
