A Formal Treatment of the Barendregt Variable Convention in Rule Inductions: Extended Abstract

MERLIN 2005

数学;计算机科学

Extended Abstract ; Michael Norrish

Others  :  http://homepages.inf.ed.ac.uk/rpollack/TYPES/MERLIN_05/p25-urban.pdf
PID  :  52669

学科分类：计算机科学（综合）

来源: CEUR

【 摘 要 】

Barendregt’s variable convention simplifies many informal proofs in the λ-calculus by allowing the consideration of only those bound variables that have been suitably chosen. Barendregt does not give a formal justification for the vari- able convention, which makes it hard to formalise such infor- mal proofs. In this paper we show how a form of the variable convention can be built into the reasoning principles for rule inductions. We give two examples explaining our technique. Categories and Subject Descriptors F.4.1 [Mathematical Logic]: Lambda-calculus and related systems; I.2.3 [De- duction and Theorem Proving]: Deduction General Terms Theory, Verification