Logický rámec - Logical framework - Wikipedia

v logika, a logický rámec poskytuje prostředky k definování (nebo prezentaci) logiky jako podpisu ve vyšším řádu teorie typů takovým způsobem, že prokazatelnost vzorce v původní logice se sníží na a obydlí typu problém v teorii rámcových typů.[1][2] Tento přístup byl úspěšně použit pro (interaktivní) automatizované dokazování věty. První logický rámec byl Automath; název této myšlenky však vychází z více známého edinburského logického rámce, LF. Několik novějších kontrolních nástrojů jako Isabelle jsou založeny na této myšlence.[1] Na rozdíl od přímého vkládání umožňuje přístup logického rozhraní mnoho logik vložených do stejného typu systému.[3]

Přehled

Logický rámec je založen na obecném zacházení se syntaxí, pravidly a důkazy pomocí a závislý typ lambda kalkulu. Syntaxe je zpracována podobným stylem, ale obecnějším než Per Martin-Löf systém umění.

K popisu logického rámce je nutné poskytnout následující:

  1. Charakterizace třídy objektové logiky, která má být reprezentována;
  2. Vhodný metajazyk;
  3. Charakterizace mechanismu, kterým jsou reprezentovány objektové logiky.

To shrnuje:

"Rámec = jazyk + reprezentace."

LF

V případě LF logický rámec, metajazykem je λΠ-kalkul. Toto je systém typů funkcí závislých na prvním řádu, které jsou spojeny pomocí princip propozic jako typů na první objednávka minimální logika. Klíčové vlastnosti kalkulu λΠ spočívají v tom, že se skládá z entit tří úrovní: objektů, typů a druhů (nebo tříd typů nebo rodin typů). to je predikativní, všechny dobře napsané výrazy jsou silně normalizující a Church-Rosser a vlastnost dobře napsaného je rozhodnutelné. Nicméně, odvození typu je nerozhodnutelný.

Logika je reprezentována v LF logický rámec mechanismem reprezentace rozsudků jako typů. To je inspirováno Per Martin-Löf vývoj společnosti Kant je pojem rozsudek, v přednáškách Siena 1983. Dva rozsudky vyššího řádu, hypotetické a generál, , odpovídají běžnému a závislému funkčnímu prostoru. Metodika rozsudků jako typů spočívá v tom, že rozsudky jsou reprezentovány jako typy jejich důkazů. A logický systém je reprezentován svým podpisem, který přiřazuje druhy a typy konečné sadě konstant, která představuje její syntaxi, její úsudky a pravidla. Pravidla a důkazy objektové logiky jsou považovány za primitivní důkazy hypoteticko-obecných soudů .

Implementaci logického rámce LF poskytuje Twelf systém na Univerzita Carnegie Mellon. Twelf zahrnuje

  • logický programovací modul
  • meta-teoretické uvažování o logických programech (ukončení, pokrytí atd.)
  • indukční metalogické věta prover

Viz také

Reference

  1. ^ A b Bart Jacobs (2001). Teorie kategorické logiky a typů. Elsevier. p. 598. ISBN  978-0-444-50853-9.
  2. ^ Dov M. Gabbay, vyd. (1994). Co je to logický systém?. Clarendon Press. p. 382. ISBN  978-0-19-853859-2.
  3. ^ Ana Bove; Luis Soares Barbosa; Alberto Pardo (2009). Language Engineering and Rigourous (sic) Software Development: International LerNet ALFA Summer School 2008, Piriapolis, Uruguay, February 24 - March 1, 2008, Revised, Selected Papers. Springer. p. 48. ISBN  978-3-642-03152-6.

Další čtení

  • Frank Pfenning (2002). "Logické rámce - krátký úvod". v Helmut Schwichtenberg, Ralf Steinbrüggen (ed.). Důkaz a spolehlivost systému (PDF). Springer. ISBN  978-1-4020-0608-1.
  • Robert Harper, Furio Honsell a Gordon Plotkin. Rámec pro definování logiky. Journal of the Association for Computing Machinery, 40 (1): 143-184, 1993.
  • Arnon Avron, Furio Honsell, Ian Mason a Randy Pollack. Použití zadaného lambda kalkulu k implementaci formálních systémů na počítači. Journal of Automated Reasoning, 9: 309-354, 1992.
  • Robert Harper. Rovnocenná formulace LF. Technická zpráva, University of Edinburgh, 1988. Zpráva LFCS ECS-LFCS-88-67.
  • Robert Harper, Donald Sannella a Andrzej Tarlecki. Prezentace strukturované teorie a logické reprezentace. Annals of Pure and Applied Logic, 67 (1-3): 113-160, 1994.
  • Samin Ishtiaq a David Pym. Relevantní analýza přirozeného odpočtu. Journal of Logic and Computation 8, 809-838, 1998.
  • Samin Ishtiaq a David Pym. Zdrojové modely Kripke závislého typu, svazku -počet. Journal of Logic and Computation 12 (6), 1061-1104, 2002.
  • Per Martin-Löf. "O významech logických konstant a důvodech logických zákonů." "Severský žurnál filozofické logiky ", 1(1): 11-60, 1996.
  • Bengt Nordström, Kent Petersson a Jan M. Smith. Programování v teorii typů Martin-Löfa. Oxford University Press, 1990. (Kniha není v tisku, ale bezplatná verze byl zpřístupněn.)
  • David Pym. Poznámka k důkazní teorii -počet. Studia Logica 54: 199-230, 1995.
  • David Pym a Lincoln Wallen. Důkazové vyhledávání v -počet. In: G. Huet a G. Plotkin (eds), Logical Frameworks, Cambridge University Press, 1991.
  • Didier Galmiche a David Pym. Důkazové vyhledávání v jazycích teoretických typů: úvod. Theoretical Computer Science 232 (2000) 5-53.
  • Philippa Gardner. Reprezentace logiky v teorii typů. Technická zpráva, University of Edinburgh, 1992. Zpráva LFCS ECS-LFCS-92-227.
  • Gilles Dowek. Nerozhodnutelnost typovatelnosti v lambda-pi-kalkulu. In M. Bezem, J.F.Groote (Eds.), Typed Lambda Calculi and Applications. Svazek 664 z Přednášky z informatiky, 139-145, 1993.
  • David Pym. Důkazy, vyhledávání a výpočet v obecné logice. Ph.D. diplomová práce, University of Edinburgh, 1990.
  • David Pym. Algoritmus sjednocení pro -počet. International Journal of Foundations of Computer Science 3 (3), 333-378, 1992.

externí odkazy