Church–Rosser Made Easy

• Autorzy: Kozen D.
• Języki publikacji: EN

Abstrakty

EN

The Church–Rosser theorem states that the λ-calculus is confluent under β-reductions. The standard proof of this result is due to Tait and Martin-Löf. In this note, we present an alternative proof based on the notion of acceptable orderings. The technique is easily modified to give confluence of the βη-calculus.

Słowa kluczowe

EN

lambda calculus; confluence; Church-Rosser theorem

• Wydawca: IOS Press
• Czasopismo: Fundamenta Informaticae
• Rocznik: 2010
• Tom: Vol. 103, nr 1-4
• Strony: 129--136
• Opis fizyczny: Bibliogr. 7 poz., wykr.

Twórcy

autor

Kozen D.

• Department of Computer Science, Cornell University, Ithaca, New York 14853-7501, USA,

Bibliografia

• [1] Barendregt, H. P.: The Lambda Calculus, Its Syntax and Semantics, 2nd edition, North-Holland, 1984.
• [2] Church, A., Rosser, J. B.: Some Properties of Conversion, Trans. Amer. Math. Soc., 39, 1936, 472-482.
• [3] Curry, H. B., Feys, R.: Combinatory Logic, vol. I, North Holland, 1958.
• [4] Hindley, R.: Standard and Normal Reductions, Trans. Amer. Math. Soc., 241, July 1978, 253-271.
• [5] Pollack, R.: Polishing up the Tait-Martin-Löf proof of the Church-Rosser theorem, Proc. De Wintermöte 95, Department of Computing Science, Chalmers University, Göteborg, Sweden, January 1995.
• [6] Sørensen, M. H., Urzyczyn, P.: Lectures on the Curry-Howard Isomorphism, vol. 149 of Studies in Logic and the Foundations of Mathematics, Elsevier, 2006.
• [7] Takahashi, M.: Parallel reductions in _-calculus (revised version), Information and Computation, 118(1), April 1995, 120-127.