Die Bemerkung bezieht sich auf eine spezifische Verwendung von Coq, nämlich die Formalisierung der Programmiersprachentheorie.
Lassen Sie uns zunächst die Unterscheidung zwischen synthetisch und analytisch klarstellen :
In einer synthetischen Herangehensweise an ein Thema sagen wir, dass es Dinge gibt, deren grundlegende Eigenschaften und Struktur auf die eine oder andere Weise postuliert werden. Wir untersuchen diese Dinge dann, indem wir uns nur auf die postulierten Eigenschaften und Strukturen stützen.
In einer analytischen Herangehensweise an ein Thema entdecken wir, dass es bestimmte Dinge gibt. Um mehr über sie zu erfahren, nehmen wir sie auseinander, untersuchen, wie sie hergestellt werden, und analysieren sie. Auf diese Weise entdecken wir ihre Eigenschaften und Struktur.
Wie würde man eine Programmiersprache auf diese zwei Arten lernen?
Synthetisch würden wir die Bestandteile der Sprache (es gibt Begriffe, es gibt Typen), ihre Grundstruktur (dies sind die Arten, Begriffe zu erstellen) und grundlegende Eigenschaften postulieren. Wir fragen nicht, woraus die Begriffe und der Typ bestehen, ob es sich bei den Begriffen um Bäume oder Zeichenfolgen handelt oder ob die Sammlung von Typen auf eine bestimmte Weise erstellt wurde.
Analytisch würden wir mit einem mathematischen Aufbau beginnen, der es uns ermöglicht, viele Dinge zu tun, beispielsweise induktive Definitionen zu verwenden, um mathematische Objekte zu konstruieren. Wir werden Begriffe und Typen als bestimmte induktiv definierte Mengen oder Typen erstellen. Dann würden wir ihre Struktur untersuchen, wie wir sie transformieren können usw.
Es sollte klar sein, dass Coq analytischer Art ist. Wenn Sie eine Programmiersprache in Coq implementieren, definieren Sie induktive Arten von Begriffen und Typen. Anschließend analysieren Sie sie mithilfe der Induktion, definieren die operative Semantik als rekursive Funktion für die Syntax von Begriffen usw.
Auf der anderen Seite ist Twelf von der synthetischen Art. Wir postulieren, dass es eine Art von Begriffen und eine Art von Typen gibt, aber wir sagen Twelf nicht , dass dies induktive Typen sind (das kann man in Twelf nicht sagen). Wir definieren die operative Semantik, indem wir grundlegende Übergangsregeln bereitstellen. Es gibt keine Erwähnung rekursiv definierter Funktionen (es gibt keine Möglichkeit, Funktionen in Twelf zu definieren), wir verlassen uns nur auf die Postulate, die wir aufgeschrieben haben.
Sie sollten die obige Situation mit der planaren Geometrie vergleichen. Hilberts Herangehensweise an die Geometrie ist synthetisch (aber seine Ideen wurzeln in Euklid), Descartes 'sind analytisch. Die analytische Geometrie wird so genannt, weil eine Linie kein primitiver Begriff ist: Sie hat eine innere Struktur, nämlich eine Menge von Punkten.
