Darstellungen Das GMETA Framework für First-Order · 2014. 2. 11. · Das GMETA Framework für...

Das GMETA Framework für First-Order Darstellungen,

Thomas Benndorf und Björn Gradowski,

Seminar Programmiersprachen

Das GMETA Framework für First-Order Darstellungen, Februar 2014

Das GMETA Framework für First-Order Darstellungen


● Grundlagen in GMeta

○ Data-generic Programming (DGP)

○ Generische Universen und induktive Familien

○ First-Order und Higher-Order

○ De Bruijn und Locally Nameless Darstellung

● Coq als Implementierungssprache

● Das Framework GMeta

○ Aufbau

○ Verwendung

○ Evaluierung und Vergleich

● Fazit

Agenda









○ Aufbau

○ Verwendung


○ Beispiel

● Fazit

Agenda


● ermöglicht Abstraktion durch generische Konzepte

● verringert die Zahl von konkreten Darstellungen

● induktive Familien und DGP ermöglichen Darstellung von

Universen

Data Generic Programming


● natürliche Zahlen:

● Listen:

● induktive Familie:

Beispiel einer induktiven Familie


Ein einfaches Universum

Abbildung: GMETA : a generic formal metatheory famework for first-order representations. Fig.7.


Das erweiterte Universum

Abbildung: GMETA : a generic formal metatheory famework for first-order representations. Fig.8.


● First Order Ansatz:

○ Identifizierung durch Benennung oder Indexierung

○ Verwendung von Namen (nominal oder locally named)

○ de Bruijn Indizes

○ locally nameless

● Higher Order Ansatz:

○ Alpha-Äquivalenz und capture avoiding substitution nur einmalig

festzulegen

○ Implementierungssprache von GMeta unterstützt HOAS nur bedingt

First Order und Higher Order


● First Order Ansatz:

○ Identifizierung durch Benennung oder Indexierung

○ Verwendung von Namen (nominal oder locally named)

○ de Bruijn Indizes

○ locally nameless

● Higher Order Ansatz:

○ Alpha-Äquivalenz und capture avoiding substitution nur einmalig

festzulegen

○ Implementierungssprache von GMeta unterstützt HOAS nur bedingt

First Order und Higher Order

nicht anwendbar


● Arten zur Darstellung von Ausdrücken mit Variablenbindung

● Einsatz bei Entwicklung formeller Metatheorien

● De Bruijn:

○ Notation für Lambda-Terme

○ Abstraktion anhand numerischer Werte

○ Grammatik: t := variable i | abstraction t | application t t

○ Beispiel: λx.x y■ => abstraction(application(variable 0)(variable 1))

■ => λ.0 1

De Bruijn und Locally Nameless


● Locally Nameless:

○ Gebundene Variablen werden numerisch dargestellt

○ Freie Variablen bekommen einen Namen

○ Grammatik: t := bvariablei | fvariablei | abstractiont | applicationt t

○ Beispiel: λx.x y■ => abstraction(application(bvariable 0)(fvariable y))

■ => λ.0 y

● beide Arten brauchen keine Alpha-Konversion => weniger Lemmas und

Definitionen

De Bruijn und Locally Nameless









○ Aufbau

○ Verwendung


○ Beispiel

● Fazit

Agenda


● Beweisassistent für Logiken höherer Ordnung

● Beinhaltet:

○ logische Sprache

○ Beweisassistent

○ Programmausführung

● zur Definition von Theoremen, Hypothesen und Lemmas

● Überprüfung auf Korrektheit

● GMeta in Coq implementiert

● wird genutzt zur Prüfung der DGP-Universen

Coq


(** The DGP universe is decidable. *)

Lemma Rep_dec : forall r r0 : Rep, {r = r0} + {r <> r0}.Proof.

decide equality.Defined.

Lemma Rep_dec_or : forall r r0 : Rep, r = r0 \/ r <> r0.Proof.

intros; elim (Rep_dec r r0); tauto.Defined.

Lemma Rep_dec_unicity : forall (r r0 : Rep)(H H0: r =r0), H = H0.Proof.

intros; auto using eq_proofs_unicity, Rep_dec_or.Qed.

Coq - Beispiel









○ Aufbau

○ Verwendung


○ Beispiel

● Fazit

Agenda


Aufbau


● Reduzierung des Wissen bzgl. DGP durch Templates und automatisch

generierte Isomorphismen

● Templates als Instanzen für Isomorphismen

○ keine Interaktion des Nutzers mit Universen nötig

○ Substitutionen und wohlgeformte Ausdrücke können genutzt werden

○ Zugriff auf vordefinierte Lemmas

● Automatisch generierte Isomorphismen werden mit Annotation-Sprache erstellt

Verwendung


Annotation-Sprache - Beispiel


● Entfaltete Operationen werden durch generischen Operationen definiert

● Beispiel von Lee et al., aus POPLMark Challenge von Aydemir et al.

Verwendung - Vorgehensweise


● Fallstudien nach Kriterien Overhead, Einstiegskosten und Transparenz

● Wissen des Nutzers bzgl. DGP und GMeta fließt in Bewertung ein

○ Basisansatz: ■ kaum Wissen zu DGP notwendig

■ Vereinfachung von Templates ähnlich der handschriftlichen Form

■ gelegentliches direktes Anwenden von Lemmas

○ Erweiterter Ansatz: ■ erweitertes Wissen zu DGP notwendig

■ manuelle Zuordnung von konkreten Definitionen zu generischen Ideen in GMeta

Bibliotheken

Evaluierung


POPLMark Challenge als Stresstest für Formalisierungstechniken

Vergleich


tbd...

Fallbeispiel


● Anforderungen werden nachweislich erfüllt

● GMeta Projekt noch weiter aktiv

● geplante Erweiterungen:

○ vollständige Universen -> Unterstützung wechselseitiger rekursiver

Datentypen

○ Unterstützung für locally named und nominal Ansätze

● zusätzliche Agda Implementierung

Fazit

Darstellungen Das GMETA Framework für First-Order · 2014. 2. 11. · Das GMETA Framework für...

Documents

Transcript of Darstellungen Das GMETA Framework für First-Order · 2014. 2. 11. · Das GMETA Framework für...