A framework for studying substitution
Abstract
This paper describes a framework for handling bound variable renaming and substitution mathematically rigorously with the aim at the same time to stay as close as possible to human intuitive preconception about the phenomena, so that proofs could be deduced from intuitive motivations more directly than in the case of standard approaches. The theory is developed for general multi-sorted term algebras with variable binding. Therefore, the results hold for a wide class of term calculi such as the λ-calculus, first-order predicate logic, the abstract syntax of programming languages etc.Downloads
Download data is not yet available.
Published
2002-01-01
How to Cite
Nestra, H. (2002). A framework for studying substitution. Acta Cybernetica, 15(4), 633-652. Retrieved from https://cyber.bibl.u-szeged.hu/index.php/actcybern/article/view/3601
Issue
Section
Regular articles