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

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

● 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

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

● 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

○ Beispiel

● Fazit

Agenda

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

● ermöglicht Abstraktion durch generische Konzepte

● verringert die Zahl von konkreten Darstellungen

● induktive Familien und DGP ermöglichen Darstellung von

Universen

Data Generic Programming

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

● natürliche Zahlen:

● Listen:

● induktive Familie:

Beispiel einer induktiven Familie

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

Ein einfaches Universum

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

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

Das erweiterte Universum

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

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

● 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

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

● 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

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

● 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

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

● 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

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

● 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

○ Beispiel

● Fazit

Agenda

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

● 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

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

(** 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

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

● 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

○ Beispiel

● Fazit

Agenda

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

Aufbau

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

● 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

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

Annotation-Sprache - Beispiel

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

● Entfaltete Operationen werden durch generischen Operationen definiert

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

Verwendung - Vorgehensweise

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

● 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

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

POPLMark Challenge als Stresstest für Formalisierungstechniken

Vergleich

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

tbd...

Fallbeispiel

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

● 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