|
|
|---|
|
|
|
|---|
Semantics of PFCSes.
A named relation denotes a predicate over a cartesian product of the prime field, where the number of factors of the cartesian product is the arity of the relation. The predicate holds exactly on the tuples of prime field elements that, when assigned to the parameters of the relation, satisfy all the constraints that define the relation. An equality constraint is satisfied when its evaluated left and right sides are equal. A relation application in the defining body of another one is satisfied when the predicate it denotes holds on the prime field elements that result from evaluating its argument expressions. There must be no recursion in the relation definitions for this to be well-defined. The body of a relation definition may include variables that are not among the formal parameters: these are regarded as existentially quantified, i.e. the predicate denoted by the relation holds on a tuple when there exist values for those extra variables that, together with the values of the tuple, satisfy all the constraints.
The semantics informally described above can be formalized, mathematically, as a function with the following characteristics. This mathematical semantic function takes the following inputs:
The mathematical semantic function returns one of the following possible outputs:
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 assignment 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.