Simplifying transformations for type-alpha certificates
Konstantine Arkoudas · DSpace@MIT (Massachusetts Institute of Technology) · 2001
This paper presents an algorithm for simplifying deductions. An array of simplifying transformations are rigorously defined. They are shown to be terminating, and to respect the formal semantics of the language. We a l so show that the transformations never increase the size or complexity of a deduction---in the worst case, they produce deductions of the same size and complexity as the original. We present several examples of proofs containing various types of superfluous "detours", andexplain how our procedure eliminates them, resulting in smaller and cleanerdeductions. All of the given transformations are fully implemented in SML-NJ. The complete code listing is presented, along with explanatory comments. Finally, although the transformations given here are defined for NDL,wepointout that they can be applied to any type-# DPL that satisfies a few simple conditions. 1.1