Instituce (počítačová věda) - Institution (computer science)
Pojem instituce vytvořil (a) Joseph Goguen a Rod Burstall v pozdních sedmdesátých letech, s cílem vyrovnat se s "populační explozí mezi EU" logické systémy použito v počítačová věda Pojem se snaží zachytit podstatu pojmu „logický systém“.[1]
Využití institucí umožňuje rozvíjet koncepty specifikační jazyky (jako strukturování specifikací, parametrizace, implementace, zdokonalování, vývoj), důkazní kameny a dokonce nástroje způsobem zcela nezávislým na základním logickém systému. Jsou tu také morfismy které umožňují spojovat a překládat logické systémy. Důležitými aplikacemi jsou opětovné použití logické struktury (nazývané také výpůjčka), heterogenní specifikace a kombinace logiky.
Šíření teorie institucionálních modelů zobecnil různé představy a výsledky teorie modelů a samotné instituce ovlivnily pokrok univerzální logika.[2][3]
Definice
Teorie institucí nepředpokládá nic o povaze logického systému. To znamená modely a věty mohou to být libovolné objekty; jediný předpoklad je, že existuje a vztah spokojenosti mezi modely a větami, které říkají, zda věta platí v modelu nebo ne. Spokojenost je inspirována Definice Tarskiho pravdy, ale ve skutečnosti to může být jakýkoli binární vztah. Klíčovým rysem institucí je, že modely, věty a jejich spokojenost jsou vždy považovány za žijící v nějakém slovníku nebo kontextu (tzv. podpis), který definuje (nelogické) symboly, které lze použít ve větách a které je třeba interpretovat v modelech. Navíc, podpisové morfismy umožnit rozšířit podpisy, změnit notaci atd. O podpisech a morfismech podpisu se nic nepředpokládá, kromě toho, že lze morfismy podpisu skládat; to znamená mít a kategorie podpisů a morfismů. Nakonec se předpokládá, že morfismy podpisu vedou k překladům vět a modelů tak, aby byla zachována spokojenost. Zatímco věty jsou překládány spolu s morfismem podpisu (myslete na to, že symboly budou nahrazeny morfismem), jsou překládány modely (nebo lépe: redukované) proti morfismy podpisu: například v případě rozšíření podpisu může být model (většího) cílového podpisu zmenšen na model (menšího) zdrojového podpisu pouhým zapomenutím na některé součásti modelu.
Formálně se instituce skládá z
- A kategorie z podpisy,
- A funktor Soubor dávat, za každý podpis , soubor věty a pro každý podpis morfismus , mapa překladu vět , kde často je psán jako ,
- A funktor Kočka dávat, za každý podpis , kategorie modely a pro každý podpis morfismus , redukční funktor , kde často je psán jako ,
- spokojenost vztah pro každého ,
takové, že pro každého v následující podmínka spokojenosti drží:
kdyby a jen kdyby
pro každého a .
Podmínka spokojenosti vyjadřuje, že pravda je neměnná při změně notace (a také při zvětšení nebo kvocientu kontextu).
Přísně vzato, funktor modelu končí v „kategorii“ všech velkých kategorií.
Příklady institucí
- Výroková logika
- Logika prvního řádu
- Logika vyššího řádu
- Intuicionistická logika
- Modální logika
- Časová logika
- Jazyk webové ontologie (SOVA)
- Společná logika
- Společný algebraický specifikační jazyk (CASL)
Viz také
Poznámky
- ^ J. A. Goguen a R. M. Burstall, Institutions: Abstract Model Theory for Specification and Programming, Journal of the Association for Computing Machinery 39, str. 95–146, 1992.
- ^ Razvan Diaconescu, „Tři desetiletí teorie institucí“ v Universal Logic: An Anlogy, editoval Jean-Yves Béziau 2012 SpringerISBN 978-3-0346-0144-3 str. 309-322
- ^ T. Mossakowski, J. A. Goguen, R. Diaconescu, A. Tarlecki, „What is a Logic?“, '. V Jean-Yves Beziau (ed.), Logica Universalis: Směrem k obecné teorii logiky, str. 113–133. Birkhäuser, Basilej, 2005, 2. vydání 2007.
Reference
- J. A. Goguen a R. M. Burstall, Introducing Institutions, Lecture Notes in Computer Science 164, pp. 221–256, 1984.
- J. Meseguer, General Logics, Logic Colloquium 87, str. 275–329, North Holland, 1989.
- J. A. Goguen a G. Rosu, Institucionální morfismy, Formální aspekty výpočtu 13, s. 274–307, 2002.
- D. Sannella a A. Tarlecki, Specifikace v libovolné instituci, Information and Computation 76, str. 165–210, 1988
- R. Diaconescu, Teorie modelu nezávislá na institucích Birkhäuser, Basilej, 2008,
externí odkazy
- „Institucionální teorie“. Internetová encyklopedie filozofie.
- Instituce Joseph Goguen
- Formalismus, logika, instituce - vztah, překlad a strukturování (včetně velké bibliografie)
- Seznam publikací Razvana Diaconesca - obsahuje nedávnou práci o teorii institucionálních modelů