Proof-tree
Fixtype of semantic proof trees.
This is a tagged union type, introduced by fty::deftagsum.
Member Tags → Types
- :equal → proof-tree-equal
- :relation → proof-tree-relation
Besides assertions (defined in assertion),
the proof system includes proofs, more precisely proof trees.
These are structures that, when properly formed,
provide proofs of assertions.
Here we only define the structure of the proof trees;
how they prove assertions is defined in exec-proof-tree.
A proof tree must have enough information that
it is easy to check whether it proves an assertion or not.
We have two kinds of proof trees:
- Proof trees that prove equality constraint assertions.
This kind of proof tree has no subtrees;
it is found at the leaves of larger proof trees.
- Proof trees that prove relation application assertions.
These include subtrees that must prove the satisfaction of
the constraints in the body that defines the relation,
for some assignment that extends the one that assigns
the values of the expressions to the formal parameters.
Let asgpara be the assignment that assigns
the values of the expressions to the formal parameters,
and let asgsub the assignment that extends asgpara
and that must satisfy all the constraints that define the relation.
Note that asgpara and asgsub are different from
the assignment asg that is
the homonymous component in the proof tree,
i.e. the one that must satisfy the relation.
The assignment asgsub is specified indirectly in the proof tree,
via the asgfree component, which is the difference
between asgsub and asgpara:
the domain of asgfree must be
disjoint from the parameters of the relation,
and must provide mappings from the non-parameter variables
used in the constraints of the relation.
All of this is formalized later;
the description just given is only a sketch.
Subtopics
- Proof-tree-case
- Case macro for the different kinds of proof-tree structures.
- Proof-tree-relation
- Proof-tree-equiv
- Basic equivalence relation for proof-tree structures.
- Proof-tree-equal
- Proof-treep
- Recognizer for proof-tree structures.
- Proof-tree-kind
- Get the kind (tag) of a proof-tree structure.
- Proof-tree-fix
- Fixing function for proof-tree structures.
- Proof-tree-count
- Measure for recurring over proof-tree structures.
