Logiki obliczalności

Logiki dla obliczalności to sformułowania logiki, które wychwytują pewien aspekt obliczalności jako podstawowe pojęcie. Zwykle obejmuje to połączenie specjalnych spójników logicznych , a także semantykę , która wyjaśnia, w jaki sposób logika ma być interpretowana w sposób obliczeniowy.

Prawdopodobnie pierwszym formalnym podejściem do logiki pod kątem obliczalności jest interpretacja realizowalności autorstwa Stephena Kleene'a w 1945 r., który przedstawił interpretację intuicjonistycznej teorii liczb w kategoriach obliczeń maszynowych Turinga . Jego motywacją było uściślenie interpretacji intuicjonizmu Heytinga-Brouwera-Kołmogorowa (BHK) , zgodnie z którą dowody twierdzeń matematycznych należy postrzegać jako konstruktywne procedury.

Wraz z pojawieniem się wielu innych rodzajów logiki, takich jak logika modalna i logika liniowa , oraz nowatorskich modeli semantycznych, takich jak semantyka gier , logikę obliczalności sformułowano w kilku kontekstach. Tutaj wspominamy o dwóch.

Logika modalna dla obliczalności

Oryginalna interpretacja Kleene'a dotycząca możliwości realizacji spotkała się z dużym zainteresowaniem wśród tych, którzy badają związki między obliczalnością a logiką. Został on rozszerzony na pełną intuicjonistyczną logikę wyższego rzędu przez Martina Hylanda w 1982 roku, który skonstruował efektywny topos . W 2002 roku Steve Awodey , Lars Birkedal i Dana Scott sformułowali logikę modalną dla obliczalności , która rozszerzyła zwykłą interpretację realizowalności o dwa operatory modalne wyrażające pojęcie „obliczalnie prawdziwe”.

Logika obliczalności Japaridze

„Logika obliczalności” to nazwa własna programu badawczego zapoczątkowanego przez Giorgi Japaridze w 2003 roku. Jego ambicją jest przebudowa logiki z semantyki teorii gier. Taka semantyka postrzega gry jako formalne odpowiedniki interaktywnych problemów obliczeniowych, a ich „prawdę” jako istnienie algorytmicznych strategii wygrywających. Zobacz logikę obliczalności .

SC Kleene. O interpretacji intuicjonistycznej teorii liczb . Journal of Symbolic Logic, 10:109-124, 1945.
JME Hylanda. Efektowny topos . W AS Troelstra i D. Van Dalen, redaktorzy, The LEJ Brouwer Centenary Symposium, strony 165-216. Wydawnictwo North Holland, 1982.
S. Awodey, L. Birkedal i DS Scott. Lokalne topy realizowalności i logika modalna obliczalności . Struktury matematyczne w informatyce, 12(3):319-334, 2002.
G. Japaridze, Wprowadzenie do logiki obliczalności . Annals of Pure and Applied Logic 123 (2003), strony 1–99.

Linki zewnętrzne

Zobacz też