There are expressions in phi-calculus, for example this one:
[ y -> [ z -> 42 ].z ].y
It may be reduced to:
[ z -> 42 ].z
And then to:
42
There is a dozen of reduction rules, which are well defined. We should implement a program, which will take an expression as an input and then show step by step how it is reduced to a normal form (when no rules can be applied any more). The output of the program should be a list of expressions, starting from the incoming expression till the normal form.
There are expressions in phi-calculus, for example this one:
It may be reduced to:
And then to:
There is a dozen of reduction rules, which are well defined. We should implement a program, which will take an expression as an input and then show step by step how it is reduced to a normal form (when no rules can be applied any more). The output of the program should be a list of expressions, starting from the incoming expression till the normal form.
I suggest we implement this in Coq.