Zum Inhalt

JDL Style Guide — Formale Notation in der Reference

Status: Draft
Geltungsbereich: Reference-Dokumente, formale Regeln, Urteilsnotation, Inferenzregeln

Warum Dieses Dokument Existiert

Die JDL Reference soll technisch, präzise und kompakt bleiben. Für viele Regeln reicht Prosa, Tabellen oder strukturierte Listen aus. Bei Typregeln, Zulässigkeitsurteilen und Ableitungen wird Prosa jedoch schnell unnötig lang, mehrdeutig oder repetitiv.

Dieses Dokument definiert daher eine kleine, feste formale Notation für die Reference:

  • für Typurteile,
  • für Wohlförmigkeit,
  • für Zulässigkeitsregeln,
  • für Label-/Closure-Aussagen,
  • und für Inferenzregeln.

Die Notation ist Hilfsmittel der Reference, nicht globaler Stil für alle JDL-Dokumente. Sie ersetzt keine lesbare Erklärung und keine JDL-Codebeispiele.

0. Grundsatz

Formale Notation wird in JDL dort verwendet, wo sie eine normative Aussage klarer und kompakter ausdrückt als reine Prosa.

Sie dient:

  • der Präzision,
  • der Wiedererkennbarkeit,
  • der Verdichtung wiederkehrender Regelmuster.

Sie dient nicht:

  • als dekorative Akademisierung,
  • als Ersatz für verständliche Lesesätze,
  • als Standardstil für VM-, IR-, Lifecycle- oder API-Dokumente.

1. Drei Schreibebenen

Die Reference unterscheidet strikt zwischen drei Ebenen.

1.1 Objektsprache JDL

Das ist echter JDL-Code.

// JDL-Code

def identity[T](x: T) -> T = x

In JDL-Codeblöcken gilt immer die normale JDL-Syntax.
Formale Metanotation darf dort nicht hineingemischt werden.

1.2 Metalanguage / Reference-Sprache

Das ist die Sprache, in der die Reference über JDL spricht.

Gamma |- e : T

Hier sind Urteile, Inferenzregeln und Relationen erlaubt und erwünscht.

1.3 Normale Prosa

Prosa erklärt:

  • Intuition,
  • Lesart,
  • Randfälle,
  • Abgrenzung zu ähnlichen Konstrukten.

Formale Regeln sollen nach Möglichkeit immer durch einen kurzen Lesesatz in normaler Sprache ergänzt werden.

2. ASCII-freundliche Autoren-Notation

In der Source-Fassung der Reference darf eine ASCII-freundliche Autoren-Notation verwendet werden. In gerenderter oder gesetzter Form darf diese in Unicode- Symbolik überführt werden.

Beispiel:

Gamma |- e : T

kann erscheinen als:

Γ ⊢ e : T

Normativ maßgeblich ist die Bedeutung, nicht die grafische Form.

2.1 Offizielle Autorenformen

Autorenform Gerenderte Form Bedeutung
Gamma Γ Kontext / Annahmen
|- ⊢ Urteil gilt unter Kontext
|= ⊨ semantische Erfüllung / Modelliertheit
-> → Implikation / Übergang / Ableitung in Metanotation
=> ⇒ definierte Konsequenz / stärkere Folgerung
/\ ∧ und
\/ ∨ oder
forall ∀ für alle
exists ∃ es existiert
!= ≠ ungleich
<= ≤ kleiner oder gleich
>= ≥ größer oder gleich
not ¬ oder not Negation
... … Auslassung

2.2 Regel

Wenn ein Symbol im Editor oder in Git den Schreibfluss behindert, ist die ASCII-Form vorzuziehen. Autoren müssen keine Unicode-Symbolik direkt eintippen, wenn dies den Schreibprozess verschlechtert.

3. Kanonische Urteilsformen

Die Reference soll nur wenige, feste Urteilsformen verwenden. Neue symbolische Formen dürfen nur eingeführt werden, wenn die vorhandenen Formen ein Problem nicht sauber ausdrücken können.

3.1 Typurteil

Gamma |- e : T

Bedeutung: Unter dem Kontext Gamma hat der Ausdruck e den Typ T.

Typische Verwendung:

  • Literale,
  • Operatoren,
  • if / match,
  • Funktionsaufrufe,
  • Cast-Regeln,
  • Ausdrücke allgemein.

3.2 Wohlförmigkeit

Gamma |- T ok
Gamma |- M ok

Bedeutung:

  • T ist ein wohlförmiger Typ,
  • M ist ein wohlförmiges Modul, Artefakt oder Konstrukt.

Typische Verwendung:

  • Typausdrücke,
  • Modul-/Plugin-Wohlförmigkeit,
  • validierte Konstruktionsformen.

3.3 Zulässigkeitsurteile

Gamma |- provide P for T ok
Gamma |- cast e -> U ok

Bedeutung: Ein bestimmtes Konstrukt ist unter den gegebenen Bedingungen zulässig.

Typische Verwendung:

  • Coherence,
  • Orphan-Regeln,
  • ForeignExtensible,
  • Cast-Zulässigkeit,
  • Plugin-spezifische Bindungsregeln.

3.4 Label-/Closure-Erfüllung

Closure(T) |= L

Bedeutung: Die geschlossene Klassifikation von T erfüllt das Label L.

Typische Verwendung:

  • Label-Inferenz,
  • Closure-Aussagen,
  • derived/sealed Garantien.

Wenn in einem Dokument bereits die bestehende Regelnotation mit proven(...), excluded(...), unproven(...), A + B -> L usw. verwendet wird, darf diese beibehalten werden. Eine Umstellung ist nur sinnvoll, wenn sie klare Vereinheitlichung bringt.

3.5 Evaluation / Reduktion

Nur verwenden, wenn dynamische Semantik wirklich formalisiert wird.

e ==> v
e -> e'

Bedeutung:

  • e ==> v für big-step evaluation,
  • e -> e' für small-step reduction.

Diese Formen sind nicht automatisch für jedes Reference-Dokument vorgesehen. Sie sollen nur eingeführt werden, wenn das jeweilige Dokument tatsächlich eine formale Auswertungssemantik beschreibt.

4. Inferenzregeln

Wenn eine Regel Voraussetzungen und eine Konklusion hat, soll sie als Inferenzregel geschrieben werden.

ASCII-Quellform:

Gamma |- e1 : Num    Gamma |- e2 : Num
--------------------------------------
Gamma |- e1 + e2 : Num

Gerenderte Form:

Γ ⊢ e1 : Num    Γ ⊢ e2 : Num
----------------------------
Γ ⊢ e1 + e2 : Num

Lesart:

Wenn e1 den Typ Num hat und e2 den Typ Num hat, dann hat e1 + e2 den Typ Num.

4.1 Terminologie

  • Oberer Teil: Prämissen
  • Unterer Teil: Konklusion
  • Gesamte Aussage: Inferenzregel

Die Begriffe „Zähler/Nenner“ o.ä. sind unzulässig.

4.2 Pflicht-Lesesatz

Jede wichtige Inferenzregel soll von einem kurzen Lesesatz in normaler Sprache begleitet werden. Formale Notation ergänzt Prosa, sie ersetzt sie nicht.

5. Wann formale Notation verwendet werden soll

Formale Notation ist empfohlen für:

  • Typregeln,
  • Cast-Regeln,
  • Coherence-/Orphan-Regeln,
  • provide-Zulässigkeit,
  • Label-/Closure-Ableitungen,
  • Effekt- und Dependency-Urteile,
  • Wohlförmigkeitsbedingungen.

Formale Notation ist nicht der Standardstil für:

  • Lifecycle-Beschreibungen,
  • Pipeline-Übersichten,
  • VM-/IR-Containerstrukturen,
  • narrative Motivation,
  • Stdlib-API-Referenzen,
  • allgemeine technische Architekturübersichten.

In solchen Fällen sind Tabellen, Listen, Zustandsdiagramme oder klare Prosa oft besser geeignet.

6. Stilregeln

6.1 Wenige Urteilsformen, viele Anwendungen

Nicht für jedes Kapitel eine neue Symbolsprache erfinden. Dieselben 3 bis 5 Urteilsformen sollen wiederverwendet werden.

6.2 Keine Symbolakrobatik

Wenn eine normative Aussage in Prosa klarer ist als in formaler Notation, dann soll Prosa verwendet werden.

6.3 JDL-Code bleibt JDL-Code

In JDL-Codeblöcken wird niemals mathematische Ersatzsyntax verwendet. Die Metalanguage darf nicht in die Objektsprache hineinbluten.

6.4 ASCII zuerst, wenn es den Schreibfluss verbessert

Autoren dürfen mit ASCII-Notation schreiben. Unicode-Renderung ist optional und sekundär.

6.5 Formale Regel plus Lesesatz

Wichtige formale Regeln sollen durch einen kurzen Lesesatz begleitet werden.

6.6 Begriffe konsistent verwenden

Die Reference verwendet für formale Regeln einheitlich folgende Begriffe:

  • Urteil
  • Kontext
  • Prämisse
  • Konklusion
  • Wohlförmigkeit
  • Zulässigkeit
  • Erfüllung

Zwischen konkurrierenden Fachbegriffen soll nicht grundlos gewechselt werden.

7. Minimale Beispielmenge

7.1 Literal-Regel

Gamma |- 42 : i32

Lesart: 42 hat den Typ i32.

7.2 Variablenregel

x : T in Gamma
--------------
Gamma |- x : T

Lesart: Wenn x im Kontext mit Typ T gebunden ist, dann hat der Ausdruck x den Typ T.

7.3 Additionsregel

Gamma |- e1 : Num    Gamma |- e2 : Num
--------------------------------------
Gamma |- e1 + e2 : Num

Lesart: Addition ist genau dann typisierbar, wenn beide Operanden Num sind.

7.4 Label-Erfüllung

Closure(T) |= Copyable

Lesart: Die geschlossene Klassifikation von T erfüllt das Label Copyable.

7.5 Coherence-Zulässigkeit

Gamma |- provide P for T ok

Lesart: Die Implementierung provide P for T ist unter den aktuellen Regeln zulässig.

8. Verhältnis zum JDL Book

Das JDL Book darf diese Notation verwenden, aber nur sparsam und immer problemgetrieben eingeführt.

Faustregel:

  • Book: Problem zuerst, Regel später
  • Reference: Regel zuerst, Erklärung knapp
  • beide dürfen dieselben Urteilsformen verwenden
  • nur die Reference ist normativ

Das Book führt zum Begriff. Die Reference fixiert die Regel.

9. Redaktionshinweis

Wenn ein Abschnitt in der Reference eine formale Regel enthält, soll geprüft werden:

  1. Ist die Aussage als Urteil oder Inferenzregel wirklich klarer?
  2. Ist dieselbe Urteilsform bereits an anderer Stelle etabliert?
  3. Gibt es einen kurzen Lesesatz direkt darunter?
  4. Wird JDL-Code und Metalanguage sauber getrennt?

Nur wenn alle vier Fragen mit „ja“ beantwortet werden können, sollte formale Notation verwendet werden.

10. Kurzfassung

Die JDL Reference verwendet formale Notation selektiv, konsistent und ASCII-freundlich.

Die wichtigsten Formen sind:

  • Gamma |- e : T
  • Gamma |- T ok
  • Gamma |- provide P for T ok
  • Closure(T) |= L

Formale Notation ist ein Präzisionswerkzeug der Reference, kein globaler Stil für alle Jade/JDL-Dokumente.