Ludyka

W teorii dowodu ludyka jest analizą zasad rządzących regułami wnioskowania logiki matematycznej . Kluczowe cechy ludyki obejmują pojęcie spójników złożonych, użycie techniki znanej jako ogniskowanie lub fokalizacja (wynaleziona przez informatyka Jeana-Marca Andreoli) oraz użycie lokalizacji lub loci nad bazą zamiast zdań .

Mówiąc dokładniej, ludyka próbuje odzyskać znane logiczne spójniki i zachowania dowodowe, postępując zgodnie z paradygmatem obliczeń interaktywnych, podobnie jak dzieje się to w semantyce gier , z którą jest ściśle związana. Abstrahując pojęcie formuł i skupiając się na ich konkretnych zastosowaniach — czyli odrębnych zdarzeniach — zapewnia abstrakcyjną składnię dla informatyki , ponieważ loci można postrzegać jako wskaźniki w pamięci.

Podstawowym osiągnięciem ludyki jest odkrycie związku między dwoma naturalnymi, ale odrębnymi pojęciami typu lub zdania.

Pierwszy pogląd, który można nazwać teorią dowodową lub interpretacją zdań w stylu Gentzena , mówi, że znaczenie zdania wynika z jego reguł wprowadzania i eliminacji. Fokalizacja udoskonala ten punkt widzenia, rozróżniając zdania pozytywne, których znaczenie wynika z zasad ich wprowadzania, oraz zdania negatywne, których znaczenie wynika z reguł ich eliminacji. W rachunkach zogniskowanych możliwe jest zdefiniowanie spójników dodatnich poprzez podanie jedynie reguł ich wprowadzenia, przy czym wybór ten wymusza kształt reguł eliminacji. (Symetrycznie, spójniki ujemne można zdefiniować w rachunkach skupionych, podając tylko reguły eliminacji, z regułami wprowadzania wymuszonymi przez ten wybór.)

Drugi pogląd, który można nazwać obliczeniową lub interpretacją zdań Brouwera-Heytinga-Kołmogorowa , przyjmuje pogląd, że z góry ustalamy system obliczeniowy, a następnie nadajemy twierdzeniom interpretację wykonalności , aby nadać im konstruktywną treść. Na przykład realizator dla twierdzenia „A implikuje B” jest obliczalną funkcją, która bierze realizatora dla A i używa go do obliczenia realizatora dla B. Modele realizowalności charakteryzują realizatorów zdań pod względem ich widocznego zachowania, a nie w pod względem ich struktury wewnętrznej.

Girard pokazuje, że dla afinicznej logiki liniowej drugiego rzędu , biorąc pod uwagę system obliczeniowy z niezakończeniem i zatrzymaniem błędów jako efektami, wykonalnością i ogniskowaniem, nadają typom to samo znaczenie.

Ludykę zaproponował logik Jean-Yves Girard . Jego artykuł wprowadzający ludykę, Locus solum: from the rules of logic to the logic of Rules , ma pewne cechy, które mogą być postrzegane jako ekscentryczne dla publikacji z logiki matematycznej (takie jak ilustracje skunksów). Należy zauważyć, że intencją tych funkcji jest narzucenie punktu widzenia Jean-Yvesa Girarda w czasie ich pisania. W ten sposób oferuje czytelnikom możliwość zrozumienia ludyki niezależnie od ich pochodzenia.

Linki zewnętrzne

1. Girard, J.-Y., Locus solum : od reguł logiki do logiki reguł (.pdf), Struktury matematyczne w informatyce , 11, 301–506, 2001.
2. Grupa czytelnicza Girarda na Carnegie-Mellon University (wiki o Locus Solum)