|
Hello,
I have written a short note about ideas that I've
thrown a few times on a blackboard.
Here is a syntactic grammar to describe derivations
in CoS (it's even more natural in Formalism A):
One point is that it is quite convenient to
describe manipulations of derivations (here it becomes term rewriting),
like those of Kai's proof of cut-elimination, which can easily be adapted to
Formalism A.
Another point is that one can identify the syntactic equations that correspond to the bureaucracy
that we'd like to get rid of.
Hence, the aim is to try and turn those
bureaucratic equations into convergent rewrite systems (maybe extending the
syntax a bit), so that normal forms get closer to the hypothetical perfect
formalism that gives us the notion of proof equality.
Well, anyway, that's the idea.
Comments, remarks, ideas, contributions, chocolates
are of course welcome,
Cheers and happy Christmas,
Stéphane Lengrand
| 