Was sind die interessantesten Äquivalenzen, die sich aus dem Curry-Howard-Isomorphismus ergeben?

97

Ich bin relativ spät in meinem Programmierleben auf den Curry-Howard-Isomorphismus gestoßen , und vielleicht trägt dies dazu bei, dass ich davon total fasziniert bin. Dies impliziert, dass es für jedes Programmierkonzept ein genaues Analogon in der formalen Logik gibt und umgekehrt. Hier ist eine "grundlegende" Liste solcher Analogien:

program/definition        | proof
type/declaration          | proposition
inhabited type            | theorem/lemma
function                  | implication
function argument         | hypothesis/antecedent
function result           | conclusion/consequent
function application      | modus ponens
recursion                 | induction
identity function         | tautology
non-terminating function  | absurdity/contradiction
tuple                     | conjunction (and)
disjoint union            | disjunction (or)          -- corrected by Antal S-Z
parametric polymorphism   | universal quantification

Also zu meiner Frage: Was sind einige der interessanteren / dunkeleren Implikationen dieses Isomorphismus? Ich bin kein Logiker, also bin ich sicher, dass ich mit dieser Liste nur die Oberfläche zerkratzt habe.

Zum Beispiel sind hier einige Programmierbegriffe, für die ich keine markigen Namen in der Logik kenne:

currying                  | "((a & b) => c) iff (a => (b => c))"
scope                     | "known theory + hypotheses"

Und hier sind einige logische Konzepte, die ich in Bezug auf die Programmierung nicht ganz festgelegt habe:

primitive type?           | axiom
set of valid programs?    | theory

Bearbeiten:

Hier sind einige weitere Äquivalenzen aus den Antworten:

function composition      | syllogism                -- from Apocalisp
continuation-passing      | double negation          -- from camccann
Tom Crockett
quelle
Abschluss ~ = Satz von Axiomen
Apocalisp
+1 Diese Frage und all die hochwertigen Antworten und Kommentare haben mich mehr über CHI gelehrt als über das, was ich über das Internet lernen konnte.
Alexandre C.
24
@ Paul Nathan:goto | jumping to conclusions
Joey Adams
Ich denke, die Menge aller gültigen Programme wäre ein Modell
Daniil
1
fst / snd | Konjunktionseliminierung, Links / Rechts | Disjunktion Einführung
Tony Morris

Antworten:

33

Da Sie ausdrücklich nach den interessantesten und dunkelsten gefragt haben:

Sie können CH auf viele interessante Logiken und Logikformulierungen erweitern, um eine wirklich große Vielfalt an Entsprechungen zu erhalten. Hier habe ich versucht, mich auf einige der interessanteren und nicht auf die dunklen zu konzentrieren, sowie auf einige grundlegende, die noch nicht aufgetaucht sind.

evaluation             | proof normalisation/cut-elimination
variable               | assumption
S K combinators        | axiomatic formulation of logic   
pattern matching       | left-sequent rules 
subtyping              | implicit entailment (not reflected in expressions)
intersection types     | implicit conjunction
union types            | implicit disjunction
open code              | temporal next
closed code            | necessity
effects                | possibility
reachable state        | possible world
monadic metalanguage   | lax logic
non-termination        | truth in an unobservable possible world
distributed programs   | modal logic S5/Hybrid logic
meta variables         | modal assumptions
explicit substitutions | contextual modal necessity
pi-calculus            | linear logic

EDIT: Eine Referenz, die ich jedem empfehlen würde, der mehr über Erweiterungen von CH erfahren möchte:

"Eine urteilsmäßige Rekonstruktion der Modallogik" http://www.cs.cmu.edu/~fp/papers/mscs00.pdf - dies ist ein großartiger Ausgangspunkt, da er von ersten Prinzipien ausgeht und vieles davon sein soll zugänglich für Nichtlogiker / Sprachtheoretiker. (Ich bin der zweite Autor, also bin ich voreingenommen.)

RD1
quelle
Vielen Dank für einige weniger triviale Beispiele (das war wirklich der Geist der ursprünglichen Frage), obwohl ich zugebe, dass einige davon über meinem Kopf liegen ... sind die Begriffe "Notwendigkeit" und "Möglichkeit" in der Logik genau definiert? Wie übersetzen sie in ihre Rechenäquivalente?
Tom Crockett
2
Ich kann auf veröffentlichte Artikel für jeden dieser Artikel verweisen, damit sie genau definiert sind. Modale Logik ist viel studiert (seit Aristoteles) und bezieht verschiedene Modi der Wahrheit - "A ist notwendigerweise wahr" bedeutet "in jeder möglichen Welt A ist wahr", während "A möglicherweise wahr ist" bedeutet "A ist wahr in einer möglichen Welt" . Sie können Dinge wie "(unbedingt (A -> B) und möglicherweise A) -> möglicherweise B" beweisen. Die modalen Inferenzregeln ergeben direkt die Ausdruckskonstrukte, Typisierungs- und Reduktionsregeln, wie in CH üblich. Siehe: en.wikipedia.org/wiki/Modal_logic und cs.cmu.edu/~fp/papers/mscs00.pdf
RD1
2
@pelotom: Vielleicht möchten Sie etwas über andere Arten von Logik lesen . Einfache klassische Logik ist in diesem Zusammenhang oft nicht nützlich - ich habe in meiner Antwort die intuitionistische Logik erwähnt, aber modale und lineare Logik sind noch "seltsamer", aber auch wirklich großartig.
CA McCann
1
Vielen Dank für die Hinweise, hört sich an, als hätte ich etwas zu lesen!
Tom Crockett
2
@ RD1: Du denkst, das ist schlecht, ich habe so viel Zeit in Haskell verbracht, dass ich Formeln der Prädikatenlogik mental in Typensignaturen übersetzen muss, bevor sie Sinn ergeben. :( Ganz zu schweigen davon, dass das Gesetz der ausgeschlossenen Mitte und dergleichen wirklich verwirrend und vielleicht verdächtig erscheint.
CA McCann
26

Sie trüben die Dinge ein wenig in Bezug auf die Nichtterminierung. Falschheit wird durch unbewohnte Typen dargestellt , die per Definition nicht unendlich sein können, da überhaupt nichts von diesem Typ zu bewerten ist.

Nichtbeendigung stellt Widerspruch dar - eine inkonsistente Logik. Eine inkonsistente Logik wird natürlich können Sie beweisen , alles , einschließlich Falschen, aber.

Ohne Berücksichtigung von Inkonsistenzen entsprechen Typsysteme typischerweise einer intuitionistischen Logik und sind notwendigerweise konstruktivistisch , was bedeutet, dass bestimmte Teile der klassischen Logik nicht direkt oder überhaupt nicht ausgedrückt werden können. Auf der anderen Seite ist dies nützlich, denn wenn ein Typ ein gültiger konstruktiver Beweis ist, ist ein Begriff dieses Typs ein Mittel, um das zu konstruieren, wovon Sie die Existenz bewiesen haben .

Ein Hauptmerkmal des konstruktivistischen Geschmacks ist, dass doppelte Negation nicht gleichbedeutend mit Nicht-Negation ist. In der Tat, Negation selten eine primitive in einem Typ - System, so dass anstelle wir es als was impliziert , Lüge darstellen kann, zB not Pwird P -> Falsity. Doppelte Negation wäre also eine Funktion mit Typ (P -> Falsity) -> Falsity, die eindeutig nicht gleichbedeutend mit etwas Typischem ist P.

Es gibt jedoch eine interessante Wendung! In einer Sprache mit parametrischem Polymorphismus erstrecken sich Typvariablen über alle möglichen Typen, einschließlich unbewohnter, so dass ein vollständig polymorpher Typ, wie er ∀a. ain gewissem Sinne fast falsch ist. Was ist, wenn wir durch Polymorphismus eine doppelte Fast-Negation schreiben? Wir bekommen einen Typ, der so aussieht : ∀a. (P -> a) -> a. Entspricht das etwas Typischem P? In der Tat ist es nur auf die Identitätsfunktion anzuwenden.

Aber worum geht es? Warum so einen Typ schreiben? Ist es Mittelwert etwas Begriffe in der Programmierung? Nun, Sie können sich das als eine Funktion Pvorstellen, die irgendwo schon etwas vom Typ hat , und Sie müssen ihr eine Funktion geben, die Pals Argument dient, wobei das Ganze im Endergebnis-Typ polymorph ist. In gewissem Sinne handelt es sich um eine angehaltene Berechnung , die darauf wartet, dass der Rest bereitgestellt wird. In diesem Sinne können diese angehaltenen Berechnungen zusammengesetzt, herumgereicht, aufgerufen werden, was auch immer. Dies sollte Fans einiger Sprachen wie Scheme oder Ruby bekannt vorkommen - denn es bedeutet, dass die doppelte Negation dem Stil der Weitergabe entsprichtund tatsächlich ist der Typ, den ich oben angegeben habe, genau die Fortsetzungsmonade in Haskell.

CA McCann
quelle
Vielen Dank für die Korrektur, ich habe "Falschheit" als Synonym für Nichtterminierung entfernt. +1 für doppelte Negation <=> CPS!
Tom Crockett
Ich verstehe nicht ganz die Intuition, ¬p als darzustellen P -> Falsity. Ich verstehe, warum es funktioniert (¬p ≡ p → ⊥), aber ich bekomme die Codeversion nicht. P -> ⊥sollte genau dann bewohnt sein, wenn Pnicht, oder? Aber sollte diese Funktion nicht immer bewohnt sein? Oder eigentlich nie möglich, da Sie eine Instanz von nicht zurückgeben können ? Ich sehe die Konditionalität nicht ganz. Was ist die Intuition hier?
Antal Spector-Zabusky
1
@Antal SZ: Die Intuition ist natürlich intuitionistische Logik! Aber ja, tatsächlich ist es schwierig, eine solche Funktion zu schreiben. Ich sehe in Ihrem Profil, dass Sie Haskell kennen. Vielleicht denken Sie also an algebraische Datentypen und Mustervergleiche? Bedenken Sie, dass ein unbewohnter Typ keine Konstruktoren haben darf und daher nichts, mit dem das Muster übereinstimmen kann. Sie müssten eine "Funktion" ohne Text schreiben, was für Haskell nicht legal ist. Meines Wissens gibt es in Haskell keine Möglichkeit, einen Begriff vom negierten Typ zu schreiben, ohne Laufzeitausnahmen oder Nichtbeendigung zu verwenden.
CA McCann
1
@Antal SZ: Wenn andererseits die äquivalente Logik konsistent ist, müssen alle Funktionen vollständig sein, z. B. muss der gesamte Mustervergleich vollständig sein. Um eine Funktion ohne Muster zu schreiben, darf der Parametertyp keine Konstruktoren haben, z. B. unbewohnt sein. Daher wäre eine solche Funktion genau und nur dann legal - und damit ihr eigener Typ bewohnt -, wenn ihre Argumentation unbewohnt ist. Daher ist eine Funktion P -> Falsitygleichbedeutend mit Pfalsch.
CA McCann
Aha, ich glaube ich verstehe. Die Version, die ich unterhalten hatte, war so etwas wie eine f x = x, die sofort instanziierbar wäre P = ⊥, aber das war eindeutig nicht generisch genug. Die Idee ist also, dass Sie keinen Körper brauchen , um einen wertlosen Typ zurückzugeben. Aber damit die Funktion definierbar und vollständig ist, brauchen Sie keine Fälle . Wenn Sie Palso unbewohnt sind, funktioniert alles? Das ist ein bisschen wackelig, aber ich glaube ich sehe es. Das scheint ziemlich seltsam mit meiner Definition des XorTyps zu interagieren ... Ich muss darüber nachdenken. Vielen Dank!
Antal Spector-Zabusky
15

Ihr Diagramm ist nicht ganz richtig; In vielen Fällen haben Sie Typen mit Begriffen verwechselt.

function type              implication
function                   proof of implication
function argument          proof of hypothesis
function result            proof of conclusion
function application RULE  modus ponens
recursion                  n/a [1]
structural induction       fold (foldr for lists)
mathematical induction     fold for naturals (data N = Z | S N)
identity function          proof of A -> A, for all A
non-terminating function   n/a [2]
tuple                      normal proof of conjunction
sum                        disjunction
n/a [3]                    first-order universal quantification
parametric polymorphism    second-order universal quantification
currying                   (A,B) -> C -||- A -> (B -> C), for all A,B,C
primitive type             axiom
types of typeable terms    theory
function composition       syllogism
substitution               cut rule
value                      normal proof

[1] Die Logik für eine Turing-vollständige Funktionssprache ist inkonsistent. Rekursion hat keine Entsprechung in konsistenten Theorien. In einer inkonsistenten Logik- / Unsound-Proof-Theorie könnte man es eine Regel nennen, die Inkonsistenz / Unsoundness verursacht.

[2] Auch dies ist eine Folge der Vollständigkeit. Dies wäre ein Beweis für ein Antisatz, wenn die Logik konsistent wäre - sie kann also nicht existieren.

[3] Existiert nicht in funktionalen Sprachen, da sie logische Merkmale erster Ordnung eliminieren: Alle Quantifizierungen und Parametrisierungen erfolgen über Formeln. Wenn Sie erste Ordnung Funktionen hätten, wäre es eine Art anders als *, * -> *usw .; die Art der Elemente der Domäne des Diskurses. Zum Beispiel in Father(X,Y) :- Parent(X,Y), Male(X), Xund YBereich über die Domäne des Diskurses (nennen wir es Dom), und Male :: Dom -> *.

Frank Atanassow
quelle
[1] - Ja, ich hätte genauer sein sollen. Ich meinte eher "strukturelle Rekursion" als uneingeschränkte Rekursion, was meiner Meinung nach dasselbe ist wie "Falten". [3] - es existiert in abhängig typisierten Sprachen
Tom Crockett
[1] Tatsache ist, dass, wenn ein Aufruf einer Rekursionsfunktion (modus ponens) nicht dazu führt, dass das Programm nicht beendet wird, die Parameter (Hypothesen), die dem Aufruf oder der Umgebung gegeben werden, zwischen diesen Aufrufen unterschiedlich sein MÜSSEN. Bei der Rekursion wird derselbe Satz also mehrmals angewendet. Wenn es etwas Besonderes gibt, ist es normalerweise das Erhöhen / Verringern von Zahlen (induktiver Schritt) und das Überprüfen mit einem vorhandenen Fall (Basisfall), was - Mathematische Induktion in der Logik entspricht.
Earth Engine
Ich mag dieses Diagramm wirklich, aber ich würde nicht "n / a" sagen, da konsistente Logik nicht die einzige Art von Logik ist, genauso wie das Beenden von Programmen nicht die einzige Art von Programm ist. Eine nicht terminierende Funktion würde einem "Zirkelargument" entsprechen und ist ein hervorragendes Beispiel für den Curry-Howard-Isomorphismus: Wenn Sie einem Zirkelargument folgen, geraten Sie in eine Endlosschleife.
Joey Adams
14
function composition      | syllogism
Apocalisp
quelle
13

Diese Frage gefällt mir sehr gut. Ich weiß nicht viel, aber ich habe ein paar Dinge (unterstützt durch den Wikipedia-Artikel , der einige nette Tabellen und dergleichen selbst enthält):

  1. Ich denke, dass Summentypen / Vereinigungstypen ( z. B. data Either a b = Left a | Right b ) einer inklusiven Disjunktion entsprechen. Und obwohl ich Curry-Howard nicht sehr gut kenne, denke ich, dass dies dies demonstriert. Betrachten Sie die folgende Funktion:

    andImpliesOr :: (a,b) -> Either a b
    andImpliesOr (a,_) = Left a
    

    Wenn ich die Dinge richtig verstehe, sagt der Typ ( a  ∧  b ) → ( a  ★  b ) und die Definition besagt, dass dies wahr ist, wobei ★ entweder inklusive oder exklusiv ist oder je nachdem, was Eitherrepräsentiert. Sie haben die EitherVertretung exklusiv oder, ⊕; jedoch ( a  ∧  b ) ↛ ( a  ⊕  b ). Zum Beispiel ⊤ ∧ ⊤ ≡ ≡, aber ⊤ ⊕ ⊥ ≡ ≡ und ⊤ ↛ ⊥. Mit anderen Worten, wenn sowohl a als auch b wahr sind, dann ist die Hypothese wahr, aber die Schlussfolgerung ist falsch, und daher muss diese Implikation falsch sein. Es ist jedoch klar, dass ( a  ∧  b ) → ( a  ∨ b ), da, wenn sowohl a als auch b wahr sind, mindestens eins wahr ist. Wenn diskriminierte Gewerkschaften eine Form der Disjunktion sind, müssen sie die inklusive Variante sein. Ich denke, dies ist ein Beweis, aber ich fühle mich mehr als frei, mich von dieser Vorstellung abzubringen.

  2. In ähnlicher Weise sind Ihre Definitionen für Tautologie und Absurdität als Identitätsfunktion bzw. nicht terminierende Funktionen etwas abweichend. Die wahre Formel wird durch den Einheitentyp dargestellt , der nur ein Element enthält ( data ⊤ = ⊤häufig geschrieben ()und / oder Unitin funktionalen Programmiersprachen). Dies ist sinnvoll: Da dieser Typ garantiert bewohnt ist und es nur einen möglichen Einwohner gibt, muss er wahr sein. Die Identitätsfunktion repräsentiert nur die bestimmte Tautologie, die a  →  a .

    Ihr Kommentar zu nicht terminierenden Funktionen ist, je nachdem, was Sie genau gemeint haben, eher falsch. Curry-Howard funktioniert auf dem Typsystem, aber die Nichtbeendigung wird dort nicht codiert. Laut Wikipedia , mit Nicht-Beendigung zu tun ist ein Thema, das Hinzufügen es inkonsequent Logik erzeugt ( zB kann ich definieren , wrong :: a -> bdurch wrong x = wrong x, und damit „beweisen“ , dass ein  →  b für alle a und b ). Wenn Sie das mit „Absurdität“ gemeint haben, dann sind Sie genau richtig. Wenn Sie stattdessen die falsche Aussage gemeint haben, dann möchten Sie stattdessen einen unbewohnten Typ, z. B. etwas, das durch definiert istdata ⊥- das heißt, ein Datentyp, der nicht konstruiert werden kann. Dies stellt sicher, dass es überhaupt keine Werte hat und daher unbewohnt sein muss, was falsch ist. Ich denke, Sie könnten wahrscheinlich auch verwenden a -> b, denn wenn wir nicht terminierende Funktionen verbieten, dann ist dies auch unbewohnt, aber ich bin nicht 100% sicher.

  3. Laut Wikipedia werden Axiome auf zwei verschiedene Arten codiert, je nachdem, wie Sie Curry-Howard interpretieren: entweder in den Kombinatoren oder in den Variablen. Ich denke, die Kombinatoransicht bedeutet, dass die primitiven Funktionen, die wir erhalten, die Dinge codieren, die wir standardmäßig sagen können (ähnlich wie modus ponens ein Axiom ist, weil die Funktionsanwendung primitiv ist). Und ich denke, dass die Variablenansicht tatsächlich dasselbe bedeuten kann - Kombinatoren sind schließlich nur globale Variablen, die bestimmte Funktionen sind. Was primitive Typen betrifft: Wenn ich richtig darüber nachdenke, dann denke ich, dass primitive Typen die Entitäten sind - die primitiven Objekte, über die wir Dinge beweisen wollen.

  4. Nach meiner Logik- und Semantikklasse wird die Tatsache, dass ( a  ∧  b ) →  c  ≡  a  → ( b  →  c ) (und auch b  → ( a  →  c )) zumindest in natürlicher Ableitung als Exportäquivalenzgesetz bezeichnet Beweise. Ich habe damals nicht bemerkt, dass es nur Curry war - ich wünschte, ich hätte es getan, denn das ist cool!

  5. Während wir jetzt eine Möglichkeit haben, eine inklusive Disjunktion darzustellen , haben wir keine Möglichkeit, die exklusive Vielfalt darzustellen. Wir sollten in der Lage sein, die Definition der exklusiven Disjunktion zu verwenden, um sie darzustellen: a  ⊕  b  ≡ ( a  ∨  b ) ∧ ¬ ( a  ∧  b ). Ich weiß nicht, wie man Negation schreibt, aber ich weiß, dass ¬ p  ≡  p  → ⊥ und sowohl Implikation als auch Falschheit einfach sind. Wir sollten daher in der Lage sein, eine ausschließliche Disjunktion darzustellen durch:

    data ⊥
    data Xor a b = Xor (Either a b) ((a,b) -> ⊥)
    

    Dies definiert den leeren Typ ohne Werte, was der Falschheit entspricht. Xorwird dann definiert, um sowohl ( und ) Eitherein a oder ein b ( oder ) als auch eine Funktion ( Implikation ) von (a, b) ( und ) bis zum unteren Typ ( falsch ) zu enthalten. Ich habe jedoch keine Ahnung, was dies bedeutet . ( Bearbeiten 1: Jetzt tue ich das, siehe nächster Absatz!) Da es keine Werte vom Typ gibt (a,b) -> ⊥(gibt es?), Kann ich nicht verstehen, was dies in einem Programm bedeuten würde. Kennt jemand eine bessere Möglichkeit, über diese oder eine andere Definition nachzudenken? ( Edit 1: Ja, Camccann .)

    Edit 1: Dank Camccanns Antwort (insbesondere der Kommentare, die er hinterlassen hat, um mir zu helfen), denke ich, dass ich sehe, was hier los ist. Um einen Wert vom Typ Typ zu Xor a berstellen, müssen Sie zwei Dinge angeben. Erstens ein Zeuge für die Existenz eines Elements von entweder aoder bals erstes Argument; das heißt, a Left aoder a Right b. Und zweitens ein Beweis dafür, dass es keine Elemente beider Arten gibt, aund b- mit anderen Worten, ein Beweis, der (a,b)unbewohnt ist - als zweites Argument. Was bedeutet es, (a,b) -> ⊥wenn dies (a,b)unbewohnt ist, wenn Sie eine Funktion nur dann schreiben können, wenn sie unbewohnt ist? Das würde bedeuten, dass ein Teil eines Objekts vom Typ ist(a,b)konnte nicht gebaut werden; mit anderen Worten, dass mindestens einer und möglicherweise beide von aund bauch unbewohnt sind! In diesem Fall könnten Sie, wenn wir über Mustervergleich nachdenken, unmöglich einen Mustervergleich für ein solches Tupel durchführen: Angenommen, das bist unbewohnt, was würden wir schreiben, das zum zweiten Teil dieses Tupels passen könnte? Daher können wir keine Musterübereinstimmung damit durchführen, was Ihnen möglicherweise hilft, zu erkennen, warum dies dazu führt, dass es unbewohnt ist. Die einzige Möglichkeit, eine Gesamtfunktion zu haben, die keine Argumente akzeptiert (wie diese muss, da sie (a,b)unbewohnt ist), besteht darin, dass das Ergebnis auch von unbewohntem Typ ist - wenn wir dies aus einer Musteranpassungsperspektive betrachten, Dies bedeutet, dass es keinen möglichen Körper gibt, obwohl die Funktion keine Fälle hat es könnte beides haben, und so ist alles in Ordnung.

Vieles davon ist, dass ich laut nachdenke / (hoffentlich) Dinge im laufenden Betrieb beweise, aber ich hoffe, dass es nützlich ist. Ich kann den Wikipedia-Artikel nur empfehlen . Ich habe es nicht detailliert durchgelesen, aber die Tabellen sind eine wirklich schöne Zusammenfassung und es ist sehr gründlich.

Antal Spector-Zabusky
quelle
1
+1 für den Hinweis, dass entweder inklusive ist oder. Beachten Sie, dass (entweder aa) ein Satz ist (für alle a).
Apocalisp
Frage zu. 2 (b): Was ist der Unterschied zwischen einem Funktionstyp, dessen einziger Bewohner nicht terminiert, und einem unbewohnten Funktionstyp? Wenn ich zum Beispiel einen Typ B ohne Konstruktoren deklarierte, definierte ich eine Funktion A-> B wie folgt: fun (a: A): B: = f (a) Dies würde in vielen Sprachen typecheck, obwohl es ist Es ist unmöglich, jemals ein B zurückzugeben. Die Funktion ist also in gewissem Sinne "bewohnt", aber ihr "Bewohner" ist absurd ... also ist sie überhaupt nicht wirklich bewohnt. Hoffe das macht irgendwie Sinn :)
Tom Crockett
3
Böden sind keine Beweise. "Es ist absurd und unmöglich anzunehmen, dass das Unwissbare und Unbestimmte enthalten und bestimmen sollte." - Aristoteles
Apocalisp
2
@ Tom: Nur um den Punkt der Nichtbeendigung nach Hause zu bringen: Wenn die Logik konsistent ist, werden alle Programme beendet . Die Nichtbeendigung tritt nur in Typsystemen auf, die inkonsistente Logiken darstellen, oder in Typensystemen für Turing-vollständige Sprachen.
CA McCann
1
Apocalisp: Either a a sollte kein Satz sein: Either ⊥ ⊥ist immer noch unbewohnt. Tom: Wie Camccann sagte, impliziert Konsistenz eine Kündigung. Ein konsistentes Typsystem erlaubt es Ihnen also nicht, sich auszudrücken f :: a -> b, und der Typ wäre unbewohnt. Ein inkonsistentes Typsystem hätte einen Einwohner für den Typ, der jedoch nicht enden würde. camccann: Gibt es inkonsistente Typsysteme, die nicht vollständig sind und einen Zwischenpunkt in der Hierarchie einnehmen? Oder ist dieser letzte Schritt (Hinzufügen einer allgemeinen Rekursion oder was auch immer) genau gleichbedeutend mit Inkonsistenz?
Antal Spector-Zabusky
12

Hier ist eine etwas dunkle, von der ich überrascht bin, dass sie nicht früher angesprochen wurde: "klassische" funktionale reaktive Programmierung entspricht zeitlicher Logik.

Wenn Sie kein Philosoph, Mathematiker oder obsessiver Funktionsprogrammierer sind, wirft dies wahrscheinlich noch einige weitere Fragen auf.

Zunächst einmal: Was ist funktionale reaktive Programmierung? Es ist eine deklarative Art, mit zeitlich variierenden Werten zu arbeiten . Dies ist nützlich, um Dinge wie Benutzeroberflächen zu schreiben, da Eingaben des Benutzers Werte sind, die sich im Laufe der Zeit ändern. "Klassisches" FRP hat zwei grundlegende Datentypen: Ereignisse und Verhaltensweisen.

Ereignisse stellen Werte dar, die nur zu diskreten Zeiten existieren. Tastenanschläge sind ein gutes Beispiel: Sie können sich die Eingaben über die Tastatur zu einem bestimmten Zeitpunkt als Zeichen vorstellen. Jeder Tastendruck ist dann nur ein Paar mit dem Zeichen der Taste und der Zeit, zu der sie gedrückt wurde.

Verhaltensweisen sind Werte, die ständig existieren, sich aber kontinuierlich ändern können. Die Mausposition ist ein gutes Beispiel: Es ist nur ein Verhalten von x, y-Koordinaten. Schließlich hat die Maus immer eine Position, und konzeptionell ändert sich diese Position kontinuierlich, wenn Sie die Maus bewegen. Schließlich ist das Bewegen der Maus eine einzige langwierige Aktion, keine diskreten Schritte.

Und was ist zeitliche Logik? Passenderweise handelt es sich um eine Reihe logischer Regeln für den Umgang mit Aussagen, die im Laufe der Zeit quantifiziert wurden. Im Wesentlichen erweitert es die normale Logik erster Ordnung um zwei Quantifizierer: □ und ◇. Das erste bedeutet "immer": Lesen Sie □ φ als "φ gilt immer". Das zweite ist "irgendwann": ◇ φ bedeutet, dass "φ irgendwann halten wird". Dies ist eine besondere Art von Modallogik . Die folgenden zwei Gesetze beziehen sich auf die Quantifizierer:

□φ ⇔ ¬◇¬φ
◇φ ⇔ ¬□¬φ

Also sind □ und ◇ auf die gleiche Weise wie ∀ und ∃ dual zueinander.

Diese beiden Quantifizierer entsprechen den beiden Typen in FRP. Insbesondere entspricht □ Verhaltensweisen und ◇ Ereignissen. Wenn wir darüber nachdenken, wie diese Typen bewohnt sind, sollte dies Sinn machen: Ein Verhalten wird zu jeder möglichen Zeit bewohnt , während ein Ereignis nur einmal auftritt.

Tikhon Jelvis
quelle
8

In Bezug auf die Beziehung zwischen Fortsetzungen und doppelter Negation ist die Art des Anrufs / cc das Peirce-Gesetz http://en.wikipedia.org/wiki/Call-with-current-continuation

CH wird normalerweise als Entsprechung zwischen intuitionistischer Logik und Programmen angegeben. Wenn wir jedoch den Call-with-Current-Continuation-Operator (callCC) hinzufügen (dessen Typ dem Peirce-Gesetz entspricht), erhalten wir eine Entsprechung zwischen klassischer Logik und Programmen mit callCC.

James Iry
quelle
4

Obwohl es sich nicht um einen einfachen Isomorphismus handelt, ist diese Diskussion über konstruktives LEM ein sehr interessantes Ergebnis. Insbesondere im Abschlussabschnitt diskutiert Oleg Kiselyov, wie die Verwendung von Monaden zur Eliminierung der doppelten Negation in einer konstruktiven Logik analog zur Unterscheidung von rechnerisch entscheidbaren Sätzen (für die LEM in einem konstruktiven Umfeld gültig ist) von allen Sätzen ist. Die Vorstellung, dass Monaden Recheneffekte erfassen, ist alt, aber diese Instanz des Curry-Howard-Isomorphismus hilft, sie ins rechte Licht zu rücken und herauszufinden, was Doppel-Negation wirklich "bedeutet".

Zaunkönig Romano
quelle
4

Mit erstklassiger Unterstützung für Fortsetzungen können Sie $ P \ lor \ neg P $ ausdrücken. Der Trick basiert auf der Tatsache, dass das Nichtaufrufen der Fortsetzung und das Beenden mit einem Ausdruck dem Aufrufen der Fortsetzung mit demselben Ausdruck entspricht.

Eine detailliertere Ansicht finden Sie unter: http://www.cs.cmu.edu/~rwh/courses/logic/www-old/handouts/callcc.pdf

Daniil
quelle
Danke für diesen Einblick!
Paulotorrens
4
2-continuation           | Sheffer stoke
n-continuation language  | Existential graph
Recursion                | Mathematical Induction

Eine Sache, die wichtig ist, aber noch nicht untersucht wurde, ist die Beziehung zwischen 2-Fortsetzungen (Fortsetzungen, die 2 Parameter annehmen ) und Sheffer-Schlaganfall . In der klassischen Logik kann der Sheffer-Strich selbst ein vollständiges Logiksystem bilden (plus einige Nicht-Operator-Konzepte). Welche das vertraute bedeutet and, or, notkann mit oder nur die Sheffer stoke umgesetzt werden nand.

Dies ist eine wichtige Tatsache der Programmtyp-Korrespondenz, da sie dazu auffordert, dass ein einzelner Typkombinator verwendet werden kann, um alle anderen Typen zu bilden.

Die Typensignatur einer 2-Fortsetzung ist (a,b) -> Void. Durch diese Implementierung können wir 1-Fortsetzung (normale Fortsetzung) als (a,a)-> Void, Produkttyp als ((a,b)->Void,(a,b)->Void)->Void, Summentyp als definieren ((a,a)->Void,(b,b)->Void)->Void. Dies gibt uns einen beeindruckenden Eindruck von seiner Ausdruckskraft.

Wenn wir weiter graben, werden wir herausfinden, dass das existentielle Diagramm von Piece einer Sprache entspricht, deren einziger Datentyp n-Fortsetzung ist, aber ich habe nicht gesehen, dass vorhandene Sprachen in dieser Form vorliegen. Es könnte also interessant sein, einen zu erfinden, denke ich.

Erdmotor
quelle