Semantics-deeply-embedded
Deeply embedded semantics of PFCSes.
The semantics informally described in semantics
can be formalized, mathematically, as a function
with the following characteristics.
This mathematical semantic function takes the following inputs:
- A list of definitions, of type definition-list.
- A constraint, of type constraint.
- An assignment,
i.e. a finite map from variables to prime field elements.
The mathematical semantic function
returns one of the following possible outputs:
- The boolean `true', indicating that,
given the input list of definitions,
the input constraint is satisfied by the input assignment.
- The boolean `false', indicating that,
given the input list of definitions,
the input constraint is not satisfied by the input assignment.
- An error, indicating that,
given the input list of definitions,
the input constraint cannot be evaluated as satisfied or not.
The third output happens when, for instance,
the constraint references
a variable that is not in the assignment,
or a relation that is not in the list of definitions.
This should never happen when the list of definitions is well-formed, as we plan to prove formally.
Attempting to define this mathematical semantic function in ACL2
runs into an issue.
A constraint that is a call of a relation is satisfied
when all the constraints that form the body of the relation are satisfied,
in some assigment that extends the one that assigns
the actual parameters to the formal parameters.
This is an existential quantification,
which is expressed via defun-sk in ACL2,
but the mathematical semantic function we are describing is recursive,
and a mutual recursion cannot involve a defun-sk in ACL2.
To overcome this issue,
we formalize a logical proof system
to derive assertions about the mathematical semantic function,
and then we define the function in ACL2 in terms of the proof system.
Subtopics
- Exec-proof-tree
- Execute a proof tree.
- Assertion-list->constr-list
- Lift assertion->constr to lists.
- Assertion-list->asg-list
- Lift assertion->asg to lists.
- Eval-expr
- Evaluate an expression, given an assignment and a prime field.
- Assertion
- Fixtype of semantic assertions.
- Eval-expr-list
- Lift eval-expr to lists.
- Assignment-for-prime-p
- Check if an assignment is for a prime field.
- Proof-outcome
- Fixtype of semantic proof outcomes.
- Proof-list-outcome
- Fixtype of semantic proof list outcomes.
- Assertion-list-from
- Lift assertion to lists.
- Definition-satp
- Check if a sequence of prime field elements
satisfies a PFCS definition.
- Assignment
- Fixtype of assignments.
- Constraint-satp
- Semantic function saying if an assignment satisfies a constraint,
given a list of definitions and a prime field.
- System-satp
- Check if an assignment satisfies a system.
- Constraint-list-satp
- Semantic function saying if an assignment
satisfies a list of constraints,
given a list of definitions and a prime field.
- Assertion-list
- Fixtype of lists of semantic assertions.
- Assignment-list
- Fixtype of lists of assignments.
- Proof-trees
