Metavariable - Metavariable
v logika, a proměnná (taky metalingvistická proměnná[1] nebo syntaktická proměnná)[2] je symbol nebo řetězec symbolů, který patří k metajazyk a znamená prvky některých jazyk objektu. Například ve větě
- Nechat A a B být dvě věty jazyka ℒ
symboly A a B jsou součástí metajazyka, ve kterém je formulován výrok o jazyce objektu ℒ.
John Corcoran považuje tuto terminologii za nešťastnou, protože zakrývá použití schémata a protože takové „proměnné“ se ve skutečnosti neomezují na doménu.[3]:220
Konvence spočívá v tom, že metavariable má být jednotně nahrazena stejnou instancí ve všech jejích vystoupeních v daném schématu. To je v rozporu s neterminální symboly v formální gramatiky kde neterminály napravo od produkce mohou být nahrazeny různými instancemi.[4]
Pokusy o formalizaci pojmu metavariable vedly k určitému druhu teorie typů.[5]
Viz také
Poznámky
- ^ lovec, str. 13.
- ^ Shoenfield 2001, str. 7.
- ^ Corcoran 2006, str. 220.
- ^ Tennent 2002, s. 36–37, 210.
- ^ Masahiko Sato, Takafumi Sakurai, Yukiyoshi Kameyama a Atsushi Igarashi. "Matematické proměnné[trvalý mrtvý odkaz ]" v Logika informatiky. 17. Mezinárodní workshop CSL 2003. 12. Výroční konference EACSL. 8. kolo Kurt Gödel, KGC 2003, Vídeň, Rakousko, 25. – 30. Srpna 2003. SborníkSpringer Přednášky z informatiky 2803. ISBN 3-540-40801-0. 484–497
Reference
- Corcoran, J. (2006). „Schémata: koncept schématu v historii logiky“ (PDF). Bulletin of Symbolic Logic. 12: 219–240.CS1 maint: ref = harv (odkaz)
- Hunter, Geoffrey. Metalogic: An Introduction to Metatheory of Standard First-Order Logic.CS1 maint: ref = harv (odkaz)
- Shoenfield, Joseph R. (2001) [1967]. Matematická logika (2. vyd.). K Peters. ISBN 978-1-56881-135-2.CS1 maint: ref = harv (odkaz)
- Tennent, R. D. (2002). Specifikace softwaru: praktický úvod. Cambridge University Press. ISBN 978-0-521-00401-5.CS1 maint: ref = harv (odkaz)