darstellungen das gmeta framework für first-order · 2014. 2. 11. · das gmeta framework für...
TRANSCRIPT
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