Wie kann man Beziehungen zwischen „Klassen“ von Typen beweisen?

8

Nachdem ich Effekte als Sitzungen, Sitzungen als Effekte gelesen hatte , fragte ich mich, wie ein Äquivalenznachweis zwischen beiden stattfinden würde oder sogar ein Beweis dafür, dass Sitzungstypen ein Typ- und Effektsystem sind.

Wie kann man allgemeiner eine Beziehung (z. B. Äquivalenz) zwischen verschiedenen "Klassen" * von Typen nachweisen? Wäre dieser Ausdruckstest von Orchard und Yoshida ausreichend?

[*]: Ich weiß nicht, wie ich es richtig definieren soll, ich möchte keine "Arten von Typen" oder "Arten von Typen" verwenden.

Cyberglot
quelle

Antworten:

6

Ein Ansatz für solche Fragen ist die Codierung .

Angenommen, Sie haben eine Sprache L1 und eine Sprache L2 und möchten zeigen, dass sie irgendwie "gleich" sind. Sie können dies tun, indem Sie eine Codierung finden

[[]]:L1L2

und zeigen Sie dann, dass für alle Programme Folgendes gilt:L1M,N

M.1N.iff[[M.1]]]]2[[M.2]]]]

Hier ist ein gewählter Begriff der Programmäquivalenz für . Um dies für typisierte Sprachen zu tun, ordnet man Typen normalerweise auch über eine Funktion die auf Typisierungsumgebungen erweitert ist, so dass etwa Folgendes gilt:ichL.ichL.1L.2

Γ1M.::αimpliziertΓ2[[M.]]]]::α
Hier ist das Typisierungsurteil für . Der gesamte Ansatz wird als vollständige Abstraktion bezeichnet .ichL.ich

Um den "Fluch der Church-Turing-Universalität" zu vermeiden, werden typischerweise Bedingungen auferlegt , z. B. dass es kompositorisch ist oder unter injektiver Umbenennung geschlossen wird. Je mehr Bedingungen erfüllt, stärker ist das vollständige Abstraktionsergebnis.[[]]]][[]]]]

Dies versuchen auch Orchard & Yoshida (Theoreme 1-5), obwohl sie es nicht ganz erreichen.

Martin Berger
quelle