A framework for studying substitution
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 t...
Elmentve itt :
Szerző: | |
---|---|
Testületi szerző: | |
Dokumentumtípus: | Cikk |
Megjelent: |
2002
|
Sorozat: | Acta cybernetica
15 No. 4 |
Kulcsszavak: | Számítástechnika, Kibernetika |
Tárgyszavak: | |
Online Access: | http://acta.bibl.u-szeged.hu/12700 |
LEADER | 01421nab a2200229 i 4500 | ||
---|---|---|---|
001 | acta12700 | ||
005 | 20220614145055.0 | ||
008 | 161015s2002 hu o 0|| eng d | ||
022 | |a 0324-721X | ||
040 | |a SZTE Egyetemi Kiadványok Repozitórium |b hun | ||
041 | |a eng | ||
100 | 1 | |a Nestra Härmel | |
245 | 1 | 2 | |a A framework for studying substitution |h [elektronikus dokumentum] / |c Nestra Härmel |
260 | |c 2002 | ||
300 | |a 633-652 | ||
490 | 0 | |a Acta cybernetica |v 15 No. 4 | |
520 | 3 | |a 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. | |
650 | 4 | |a Természettudományok | |
650 | 4 | |a Számítás- és információtudomány | |
695 | |a Számítástechnika, Kibernetika | ||
710 | |a Finno-Ugoric Symposium on Programming Languages and Software Tools (7.) (2001) (Szeged) | ||
856 | 4 | 0 | |u http://acta.bibl.u-szeged.hu/12700/1/cybernetica_015_numb_004_633-652.pdf |z Dokumentum-elérés |