The Functional Interpretation of Direct Computations

The concept of direct computation used by Statman (1977) was instrumental in the development of a notion of normal form for proofs of equality. In order to find a functional (Curry–Howard style) interpretation of direct computations we take a closer look at proof procedures for first-order sentences with equality drawing the attention to the need for introducing (function) symbols for rewrites. This leads us to a proposal to the effect that the framework of labelled natural deduction gives the right tools to formulate a proof theory for the “logical connective” of propositional equality in the style of the so-called Curry–Howard interpretation. The basic idea is that when analysing an equality sentence into (i) proof conditions (introduction) and (ii) immediate consequences (elimination), it becomes clear that we need to bring in identifiers (i.e. function symbols) for sequences of rewrites, and this is what we claim is the missing entity in P. Martin-Löfʼs equality types (both intensional and extensional). For the proof system for equality we establish a normalisation procedure, proving that it is terminating and confluent.1