The functional interpretation of direct computations.

*(English)*Zbl 1347.03062
Haeusler, Edward Hermann (ed.) et al., Proceedings of the 5th workshop on logical and semantic frameworks, with applications (LSFA 2010), Natal, Brazil, August 31, 2010. Amsterdam: Elsevier. Electronic Notes in Theoretical Computer Science 269, 19-40 (2011).

Summary: The concept of direct computation used by Statman 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) [in: Proc. 3rd Scand. Logic Symp., Uppsala 1973, 81–109 (1975; Zbl 0334.02017)]. For the proof system for equality we establish a normalisation procedure, proving that it is terminating and confluent.

For the entire collection see [Zbl 1281.68027].

For the entire collection see [Zbl 1281.68027].

PDF
BibTeX
XML
Cite

\textit{R. J. G. B. de Queiroz} and \textit{A. G. de Oliveira}, Electron. Notes Theor. Comput. Sci. 269, 19--40 (2011; Zbl 1347.03062)

Full Text:
DOI

##### References:

[1] | Aczel, P.H.G., Frege structures and the notions of proposition, truth and set, (), 31-59, xx+425pp. Proceedings of the Symposium held in June 18-24, 1978, at Madison, Wisconsin, USA |

[2] | Aczel, P.H.G., Term declaration logic and generalised composita, (), 22-30, Proceedings of the Symposium held July 15-18 1991, in Amsterdam, The Netherlands |

[3] | Barendregt, H.P., The lambda calculus, its syntax and semantics, (), revised edition · Zbl 0467.03010 |

[4] | Errett, Bishop, Foundations of constructive analysis, Mcgraw-Hill series in higher mathematics, (1967), McGraw-Hill Book Company New York, xiv+371pp · Zbl 0195.30404 |

[5] | Le Chenadec, Ph., On the logic of unification, J. symbolic computation, 8, 1 and 2, 141-199, (July/August 1989) |

[6] | Gabbay, D.M., Labelled deductive systems, volume I - foundations, (1996), Oxford University Press |

[7] | Gabbay, D.M.; de Queiroz, R.J.G.B., Extending the curry-howard interpretation to linear, relevant and other resource logics, The journal of simbolic logic, 57, 4, 1319-1365, (December 1992) |

[8] | Hindley, J.R.; Seldin, J.P., Lambda calculus and combinators. an introduction, (2008), Cambridge University Press · Zbl 1149.03016 |

[9] | M. Hofmann and T. Streicher. The groupoid model refutes uniqueness of identity proofs. In Logic in Computer Science, 1994 (LICS ʼ94), pp. 208-212, 1994. |

[10] | Howard, W.A., The formulae-as-types notion of construction, (), xxv+606pp |

[11] | Kreisel, G.; Tait, W., Finite definability of number theoretic functions and parametric completeness of equational calculi, Zeitschr. f. math. logik und grundlagen d. math, 7, 28-38, (1961) · Zbl 0116.00506 |

[12] | Martin-Löf, P., About models for intuitionistic type theories and the notion of definitional equality, (), 81-109, Symposium held in 1973 |

[13] | Martin-Löf, P., An intuitionistic theory of types: predicative part, (), 73-118, viii+513pp, 1975. Proceedings of the Colloquium held in Bristol, UK · Zbl 0334.02016 |

[14] | Martin-Löf, P., Constructive mathematics and computer programming, (), 153-175, xiii+738pp, 1992. Proceedings of the International Congress held in Hannover |

[15] | P. Martin-Löf. Intuitionistic Type Theory. Series Studies in Proof Theory. Bibliopolis Naples, iv+91pp., 1984. Notes by Giovanni Sambi of a series of lectures given in Padova, June 1980. |

[16] | Mitchell, J.C.; Scedrov, A., Notes on sconing and relators, (), 352-378, Available by anonymous ftp from host · Zbl 0795.03100 |

[17] | Nordström, B.; Petersson, K.; Smith, J.M., Programming in martin-Löfʼs type theory. an introduction, The international series of monographs on computer science, Vol. 7, (1990), Clarendon Press Oxford, x+221pp |

[18] | A. G. de Oliveira. Proof Transformations for Labelled Natural Deduction via Term Rewriting. (In Portuguese). Masterʼs thesis, Depto. de Informática, Universidade Federal de Pernambuco, C.P. 7851, Recife, PE 50732-970, Brasil, April 1995. |

[19] | de Oliveira, A.G.; de Queiroz, R.J.G.B., Term rewriting systems with labelled deductive systems, (), 59-72 |

[20] | de Oliveira, A.G.; de Queiroz, R.J.G.B., A normalization procedure for the equational fragment of labelled natural deduction, Logic journal of the interest group in pure and applied logics, 7, 2, 173-215, (1999) · Zbl 0923.03064 |

[21] | de Oliveira, A.G.; de Queiroz, R.J.G.B., A new basic set of proof transformations, (), 499-528 · Zbl 1272.03153 |

[22] | de Queiroz, R.J.G.B., A proof-theoretic account of programming and the rôle of reduction rules, Dialectica, 42, 4, 265-282, (1988) · Zbl 0676.03007 |

[23] | de Queiroz, R.J.G.B., The mathematical language and its semantics: to show the consequences of a proposition is to give its meaning, (), 259-266, Symposium held in Kirchberg/Wechsel, Austria, August 14-21 1988 |

[24] | de Queiroz, R.J.G.B., Meaning as grammar plus consequences, Dialectica, 45, 1, 83-86, (1991) |

[25] | R. J. G. B. de Queiroz. Grundgesetze alongside Begriffsschrift (abstract). In Abstracts of Fifteenth International Wittgenstein Symposium. pp. 15-16. Symposium held in Kirchberg/Wechsel, August 16- 23 1992. |

[26] | de Queiroz, R.J.G.B., Normalisation and language-games, Dialectica, 48, 2, 83-125, (1994) |

[27] | de Queiroz, R.J.G.B., Meaning, function, purpose, usefulness, consequences - interconnected concepts, Logic journal of the interest group in pure and applied logics, 9, 5, 693-734, (2001) · Zbl 0989.03006 |

[28] | de Queiroz, R.J.G.B., On reduction rules, meaning as use, and proof-theoretic semantics, Studia logica, 90, 2, 211-247, (November 2008) |

[29] | R. J. G. B. de Queiroz and D. M. Gabbay. Equality in Labelled Deductive Systems and the functional interpretation of propositional equality. In P. Dekker and M. Stokhof, editors, Proceedings of the 9th Amsterdam Colloquium, pages 547-546, 1994. |

[30] | de Queiroz, R.J.G.B.; Gabbay, D.M., The functional interpretation of the existential quantifier, Bulletin of the interest group in pure and applied logics, Jsl, 58, 2, 753-754, (1993), (Presented at Logic Colloquium ʼ91, Uppsala, August 9-16.) |

[31] | de Queiroz, R.J.G.B.; Gabbay, D.M., The functional interpretation of modal necessity, (), 61-91 · Zbl 0911.03012 |

[32] | de Queiroz, R.J.G.B.; Gabbay, D.M., Labelled natural deduction, (), 173-250 · Zbl 0954.03008 |

[33] | R. J. G. B. de Queiroz, D. M. Gabbay, and A. G. de Oliveira. The Functional Interpretation of Logical Deduction, Imperial College Press, World Scientific, to appear. · Zbl 1248.03003 |

[34] | R. J. G. B. de Queiroz and A. G. de Oliveira. Natural Deduction for Equality: The Missing Entity. In Advances in Natural Deduction, E. H. Haeusler, L. C. Pereira & V. de Paiva (eds.), a volume of the series Trends in Logic, Kluwer/Springer, 2010, to appear. · Zbl 1339.03052 |

[35] | Statman, R., Herbrandʼs theorem and gentzenʼs notion of a direct proof, () |

[36] | Statman, R., Bounds for proof-search and speed-up in the predicate calculus, Annals of mathematical logic, 15, 225-287, (1978) · Zbl 0411.03047 |

[37] | Troelstra, A.S.; van Dalen, D., Constructivism in mathematics: an introduction. vol. II, Studies in logic and the foundations of mathematics, Vol. 123, (1988), North-Holland Amsterdam, xvii+535pp · Zbl 0661.03047 |

This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.