순차식 연산 (Sequent calculus) 과 절단제거 (Cut elimination)
Sequent Calculus and Cut-Elimination
0
조회
0
다운로드
0
인용
0
참고문헌
키워드
초록
순차식 연산은 겐첸이 자연연역을 1934년 대칭적 버전으로 재구성한 것으로서, 여기에서 그는 ‘주정리’ 를 소개한다. 이 논문에서 우리는 절단의 유용성에도 불구하고 증명이론에서 왜 절단정리가 이토록 중요한 위상을 차지하는지 검토할 것이다. 이어서 커리-하우어드 대응의 역동적 측면, 즉 절단 제거와 단순히 유형화된 람다-연산에서 -환원의 대응이 연구될 것이다. 이러한 대응의 중요성은 프로그램의 세계와 수학적 증명의 세계를 마주보게 함으로써 프로그램의 정확성을 보증해준다는 데에 있다
Abstract
Sequent Calculus is a symmetrical version of the Natural Deduction which Gentzen restructured in 1934, where he presents ‘Hauptsatz’. In this thesis, we will examine why the Cut-Elimination Theorem has such an important status in Proof Theory despite of the efficiency of the Cut Rule. Subsequently, the dynamic side of Curry-Howard correspondence which interprets the system of Natural Deduction as ‘Simply typed λ- calculus’, so to speak the correspondence of Cut-Elimination and β-reduction in λ-calculus,will also be studied. The importance of this correspondence lies in matching the world of program and the world of mathematical proof. Also it guarantees the accuracy of program.
참고문헌 (18)
- P. Benacerraf, "Philosophy of Mathematics" (2002), 아카넷
- T. Coquand, "The Calculus of Construction", Information and Computation, 76, pp.95~120 (1988)
- R. David, "Introduction à la logique. in: Théorie de la démonstration" (2001), Dunod
- G. Dowek, "Les métamorphose du calcul: une étonnante histoire de mathématiques" (2007), Le Pommier
- G. Gentzen, "Recherches sur la déduction logique" (1955), PUF
- Girard, Lafont, "Proofs and types" (1989), Cambridge University Press
- R. Hindley, "Introduction to combinator and -calculus" (1986), Cambridge University Press
- J.-L. Krivine, "Lambda-Calcul" (1990), Masson
- D. Prawitz, "Natural deduction" (1965), Almquist & Wiksell
- A. Turing, "La machine de Turing" (1995), Seuil
- "Théorie de la déduction"[URL]
- "On the Correspondance between proofs and -Term"[URL]
- "Leçons de mathématiques d’aujourd’hui, la Théorie de la démonstration"[URL]
- "Du Pouquoi au comment: la Théorie de la démonstration de 1950 à nos jours"[URL]
- "Théorie de la démonstration"[URL]
- G. Longo, "Proposition et Types", ~
- A. R. Omond, "Proof Normalization I: Gentzen’s Hauptsatz", ~ (1993)
- J.-P. Roy, "Initiaiton à la Programmation Fonctionnelle", ~ (2006)