Permutations and computations

Roy Dyckhoff
School of Mathematical & Computational Sciences, 
St Andrews University, St Andrews, Scotland
rd@dcs.st-and.ac.uk
Abstract. We consider the surjective Prawitz translation f from (sequent calculus) cut-free derivations to (natural) normal deductions, in order to examine the relationship between the uniform sequent calculus derivations of Miller, Nadathur, Pfenning & Scedrov [4] and the normal natural deductions of Prawitz [6,7] for first-order minimal logic. We conjecture (but cannot yet prove) that f identifies two such derivations iff they are permutation-equivalent, in the sense of Kleene’s work [1] on permutations of intuitionistic derivations, a result similar to work of Zucker [8] on permutative conversions (for the system with cut and without the constants for disjunction and existential quantification). For the restricted language fohH of first-order hereditary Harrop sequents (no occurrences of disjunctions or existential quantifiers that would trigger use of /L or $L), we show (i) that f maps the uniform derivations of [4] onto the set EN of deductions in [6] expanded normal form; and (ii) (if the conjecture is true) that f identifies two such derivations iff they are permutation-equivalent using just the permutations involving _L, &L and "L. Third, restricting even further to the language D of definite formulae and goals, we show (i) that f maps the simple uniform derivations of Miller [2] onto EN and (ii) (again, if the conjecture is true) that f identifies two such derivations iff they are permutation-equivalent using just the permutations involving &L and "L. This gives a bijection (also studied in [5]) from the set of uniform proofs with backchaining (a system [3] intermediate between sequent calculus and natural deduction) onto EN. 
Thus, the logic programmer’s restriction to the use for D of uniform proofs with backchaining is complete not merely (as is well-known) w.r.t. derivability but also, in a bijective fashion, w.r.t. the construction of expanded normal deductions. We anticipate these ideas to be useful in a proof-theoretic integration of functional and logic programming (based on natural deduction and sequent calculus respectively).

[1]	Kleene, S. C.:  Permutability of inferences in Gentzen’s calculi LK and LJ, Mem. Amer. Math. Soc. (1952), 1–26.
[2]	Miller, D.: A logical analysis of modules in logic programming, J. Logic Programming 6 (1989), 79–108.
[3]	Miller, D.: Abstractions in logic programs, in: Odifreddi, P. (editor), Logic and computer science, vol. 31 of APIC Studies in Data Processing, Academic Press 1990, 329–359.
[4]	Miller, D., G. Nadathur, F. Pfenning & A. Scedrov : Uniform proofs as a foundation for logic programming, Annals of Pure and Applied Logic 51 (1991), 125–157.
[5]	Pfenning, F.: Unpublished lecture notes, 1994.
[6]	Prawitz, D.: Natural deduction, Almquist & Wiksell, Stockholm 1965.
[7]	Prawitz, D.: Ideas and results in proof theory, in: Fenstad, J. E.: Proc. of the second Scandinavian logic symposium, North-Holland 1971, 235–308.
[8]	Zucker, J.: The correspondence between cut-elimination and normalization, Annals of Mathematical Logic 7 (1974), 1–112.