We need to ensure that all the definable fixed points still maintain the normalisation procedure. And so we will have to restrict fixed points to certain kinds of operators, the ones in which the variable occurs only in positive positions.
| We see now
some more details about Gallina and especially about the inductive definition
items. First of all we have a powerful definition by case analysis. And
then we may define recursive and co-recursive terms. Fix is the operator
for defining recursive terms; CoFix is for co-recursion. It is clear that
we cannot have arbitrary fixed points, since the strong normalisation property
is the crucial issue for the correctness of the system. We need to ensure that all the definable fixed points still maintain the normalisation procedure. And so we will have to restrict fixed points to certain kinds of operators, the ones in which the variable occurs only in positive positions. |
|
