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 reichen Prosa, Tabellen oder strukturierte Listen aus. Bei Typregeln, Zulässigkeitsurteilen, Context-Erfüllung und Ableitungen wird Prosa jedoch schnell lang, mehrdeutig oder repetitiv.

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

  • für Typurteile,
  • für Wohlförmigkeit,
  • für Zulässigkeitsregeln,
  • für Namespace-, Scope- und Context-Aussagen,
  • für Effect-/Dependency-Urteile,
  • für Label-/Closure-Aussagen,
  • und für Inferenzregeln.

Die Notation ist ein Hilfsmittel der Reference, kein 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, kürzer und eindeutiger ausdrückt als reine Prosa.

Sie dient:

  • der Präzision,
  • der Wiedererkennbarkeit,
  • der Verdichtung wiederkehrender Regelmuster,
  • der sauberen Trennung von Objektsprache und Metasprache.

Sie dient nicht:

  • als dekorative Akademisierung,
  • als Ersatz für verständliche Lesesätze,
  • als Standardstil für VM-, IR-, Lifecycle- oder API-Dokumente,
  • als Einladung, jedes Kapitel mit eigener Symbolsprache zu ruinieren.

Jede wichtige formale Regel soll einen kurzen Lesesatz erhalten. Wer eine Regel nicht in normaler Sprache erklären kann, hat keine präzise Regel, sondern nur hübsch gesetzte Verwirrung.

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.

Wichtig:

// Funktionstyp in JDL:
type Handler = (Request) -> Response

// Cast-Ausdruck in JDL:
val response = user -> UserResponse

Die Metasprache darf diese Unterscheidung nicht verwischen. In JDL-Code bedeutet (T) -> U ein Funktionstyp. x -> U ist ein Cast-Ausdruck.

1.2 Metalanguage / Reference-Sprache

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

ASCII-Autorenform:

Gamma |- e : T

Gerenderte mathematische Form:

\[ \Gamma \vdash e : T \]

Hier sind Urteile, Inferenzregeln und Relationen erlaubt.

Die Metalanguage beschreibt JDL. Sie ist nicht selbst JDL.

1.3 Normale Prosa

Prosa erklärt:

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

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

2. Der formale Kontext Gamma

Gamma / Γ ist der formale Urteilskontext der Reference.

Er ist nicht identisch mit einem JDL-context.

Ein JDL-context ist eine Komponente innerhalb von Gamma.

Diese Unterscheidung ist wichtig, weil JDL selbst die Begriffe Namespace, Scope und Context trennt:

  • Namespace adressiert Symbole.
  • Scope bestimmt sichtbare Bindings.
  • Context bestimmt geltende Ausführungsbedingungen.
  • Gamma bündelt die formalen Annahmen, unter denen eine Regel gilt.

Konzeptionell kann Gamma folgende Komponenten enthalten:

Gamma.ns      Namespace-Umgebung
Gamma.scope   lokale Namensbindungen
Gamma.ctx     aktueller JDL-Context / ContextDescriptor
Gamma.types   TypeEnvironment / bekannte TypeDescriptors
Gamma.labels  Label-/Closure-Umgebung
Gamma.meta    weitere dokumentabhängige Annahmen

Kurzform:

Gamma = { ns, scope, ctx, types, labels, meta, ... }

In LaTeX-Schreibweise darf für Komponenten die Punktform verwendet werden:

\[ \Gamma = \{\mathsf{ns}, \mathsf{scope}, \mathsf{ctx}, \mathsf{types}, \mathsf{labels}, \mathsf{meta}, \ldots\} \]

Diese Struktur ist erklärend. Sie schreibt keine konkrete Implementierungsform für Compiler oder TypeEngine vor.

2.1 Abgrenzung: Gamma vs. JDL-context

Gamma ist ein Begriff der formalen Reference-Sprache.

context ist ein Begriff der JDL-Objektsprache.

Sie dürfen nicht gleichgesetzt werden.

Richtig:

Gamma.ctx |= D

LaTeX:

\[ \Gamma.\mathsf{ctx} \vDash D \]

Bedeutung: Der aktuelle JDL-Context innerhalb von Gamma erfüllt die Dependency-Row D.

Falsch:

context |= D

wenn context nicht vorher als formaler Name gebunden wurde.

In Prosa darf gesagt werden:

Der aktuelle JDL-Context erfüllt D.

In formaler Notation soll diese Aussage als Gamma.ctx |= D geschrieben werden.

2.2 Komponenten gezielt verwenden

Die Komponenten von Gamma sollen nur dann ausgeschrieben werden, wenn die Regel sie wirklich unterscheidet.

Allgemeines Typurteil:

Gamma |- e : T

LaTeX:

\[ \Gamma \vdash e : T \]

Lokales Binding:

x : T in Gamma.scope
--------------------
Gamma |- x : T

LaTeX:

\[ \frac{x : T \in \Gamma.\mathsf{scope}}{\Gamma \vdash x : T} \]

Context-Erfüllung:

Gamma.ctx |= D

LaTeX:

\[ \Gamma.\mathsf{ctx} \vDash D \]

Namespace-Auflösung:

s resolves to q in Gamma.ns
q : T in Gamma.types
------------------------
Gamma |- s : T

LaTeX:

\[ \frac{ s \rightsquigarrow q \in \Gamma.\mathsf{ns} \qquad q : T \in \Gamma.\mathsf{types} }{ \Gamma \vdash s : T } \]

Wenn eine Regel keine Unterscheidung zwischen Namespace, Scope und Context braucht, soll sie einfach Gamma verwenden. Nicht jede Regel braucht eine Inventarliste aller Compilerabteilungen. Die haben Besseres zu tun. Angeblich.

3. Schreibformen: ASCII, Unicode und LaTeX

Die Source-Fassung der Reference darf ASCII-freundlich bleiben. Gerenderte oder gesetzte Fassungen dürfen Unicode oder LaTeX verwenden.

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

3.1 Empfohlene Schreibstrategie

Für normale Markdown-Source ist ASCII oft am angenehmsten:

Gamma |- e : T

Für gerenderte Reference-Seiten mit MathJax darf LaTeX verwendet werden:

\[
\Gamma \vdash e : T
\]

Gerendert:

\[ \Gamma \vdash e : T \]

Die ASCII-Form bleibt die kanonische Autorenform. Die LaTeX-Form ist die kanonische Renderform für Dokumente, in denen MathJax aktiviert ist.

3.2 Offizielle Autoren- und Renderformen

Autorenform Unicode LaTeX Bedeutung
Gamma Γ \Gamma formaler Urteilskontext / Annahmen
Gamma.ns Γ.ns \Gamma.\mathsf{ns} Namespace-Komponente des Urteilskontexts
Gamma.scope Γ.scope \Gamma.\mathsf{scope} lokale Scope-/Binding-Komponente
Gamma.ctx Γ.ctx \Gamma.\mathsf{ctx} aktueller JDL-Context / ContextDescriptor
Gamma.types Γ.types \Gamma.\mathsf{types} bekannte TypeDescriptors / TypeEnvironment
Gamma.labels Γ.labels \Gamma.\mathsf{labels} Label-/Closure-Umgebung
|- ⊢ \vdash Urteil gilt unter Kontext
|= ⊨ \vDash semantische Erfüllung / Modelliertheit
-> → \to Implikation / Übergang / Ableitung in Metanotation
=> ⇒ \Rightarrow definierte Konsequenz / stärkere Folgerung
/\ ∧ \land und
\/ ∨ \lor oder
forall ∀ \forall für alle
exists ∃ \exists es existiert
!= ≠ \ne ungleich
<= ≤ \le kleiner oder gleich
>= ≥ \ge größer oder gleich
not ¬ oder not \neg Negation
... … \ldots Auslassung

3.3 LaTeX-Delimiter

Für MkDocs Material mit MathJax sollen folgende Delimiter verwendet werden:

Inline:

\(\Gamma \vdash e : T\)

Gerendert: \(\Gamma \vdash e : T\)

Block:

\[
\Gamma \vdash e : T
\]

Gerendert:

\[ \Gamma \vdash e : T \]

In der Markdown-Datei steht genau ein Backslash vor (, ), [ und ]. Nicht \\( schreiben. Doppelte Backslashes sind kein Ausdruck tieferer Mathematik, sondern nur ein kleiner Unfall mit größerer Wirkung.

3.4 MkDocs-/Material-Hinweis

Für gerenderte LaTeX-Notation in MkDocs Material wird empfohlen:

markdown_extensions:
  - pymdownx.arithmatex:
      generic: true

extra_javascript:
  - javascripts/mathjax.js
  - https://unpkg.com/mathjax@3/es5/tex-mml-chtml.js

docs/javascripts/mathjax.js:

window.MathJax = {
  tex: {
    inlineMath: [["\\(", "\\)"]],
    displayMath: [["\\[", "\\]"]],
    processEscapes: true,
    processEnvironments: true
  },
  options: {
    ignoreHtmlClass: ".*|",
    processHtmlClass: "arithmatex"
  }
};

document$.subscribe(() => {
  MathJax.startup.output.clearCache();
  MathJax.typesetClear();
  MathJax.texReset();
  MathJax.typesetPromise();
});

Der document$.subscribe-Block ist wichtig, wenn Material Instant Loading nutzt. Sonst rendert MathJax gern genau dann nicht, wenn man es gerade jemandem zeigen will. Also: klassisches Webzeug, nur mit mehr griechischen Buchstaben.

4. 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.

4.1 Typurteil

ASCII:

Gamma |- e : T

LaTeX:

\[ \Gamma \vdash 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.

4.2 Wohlförmigkeit

ASCII:

Gamma |- T ok
Gamma |- M ok

LaTeX:

\[ \Gamma \vdash T\ \mathsf{ok} \]
\[ \Gamma \vdash M\ \mathsf{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,
  • Blueprint- und Record-Shape-Formen.

4.3 Zulässigkeitsurteile

ASCII:

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

LaTeX:

\[ \Gamma \vdash \mathsf{provide}\ P\ \mathsf{for}\ T\ \mathsf{ok} \]
\[ \Gamma \vdash \mathsf{cast}\ e \to U\ \mathsf{ok} \]

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

Typische Verwendung:

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

Hinweis: cast e -> U ist Metanotation für die Cast-Zulässigkeit. In JDL-Code bleibt e -> U der Cast-Ausdruck.

4.4 Label-/Closure-Erfüllung

ASCII:

Closure(T) |= L

LaTeX:

\[ \mathsf{Closure}(T) \vDash 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.

4.5 Context- und Dependency-Erfüllung

ASCII:

Gamma.ctx |= D

LaTeX:

\[ \Gamma.\mathsf{ctx} \vDash D \]

Bedeutung: Der aktuelle JDL-Context innerhalb von Gamma erfüllt die Dependency-Row D.

Typische Verwendung:

  • Effect[R, E, D],
  • Service-/Capability-Anforderungen,
  • Blueprint-Ausführung,
  • Engine-Zulässigkeit,
  • ContextBridge-Regeln.

Beispiel:

Gamma |- eff : Effect[R, E, D]
Gamma.ctx |= D
-----------------------------
Gamma |- run(eff) : Result[R, E]

LaTeX:

\[ \frac{ \Gamma \vdash \mathit{eff} : \mathsf{Effect}[R, E, D] \qquad \Gamma.\mathsf{ctx} \vDash D }{ \Gamma \vdash \mathsf{run}(\mathit{eff}) : \mathsf{Result}[R, E] } \]

Lesart: Wenn eff ein Effect ist, der Dependencies D benötigt, und der aktuelle JDL-Context diese Dependencies erfüllt, dann darf eff ausgeführt werden und liefert Result[R, E].

4.6 Namespace- und Scope-Aussagen

Namespace- und Scope-Regeln sollen nicht als bloße Typregeln verkleidet werden, wenn die Unterscheidung relevant ist.

Lokaler Scope:

x : T in Gamma.scope
--------------------
Gamma |- x : T

LaTeX:

\[ \frac{x : T \in \Gamma.\mathsf{scope}}{\Gamma \vdash x : T} \]

Namespace-Auflösung:

s resolves to q in Gamma.ns
q : T in Gamma.types
------------------------
Gamma |- s : T

LaTeX:

\[ \frac{ s \rightsquigarrow q \in \Gamma.\mathsf{ns} \qquad q : T \in \Gamma.\mathsf{types} }{ \Gamma \vdash s : T } \]

Lesart: Lokale Namen werden über Gamma.scope gebunden. Qualifizierte oder importierte Symbole werden über Gamma.ns aufgelöst und anschließend in Gamma.types typisiert.

4.7 Evaluation / Reduktion

Nur verwenden, wenn dynamische Semantik wirklich formalisiert wird.

ASCII:

e ==> v
e -> e'

LaTeX:

\[ e \Downarrow v \]
\[ e \to e' \]

Bedeutung:

  • e ==> v / \(e \Downarrow v\) für big-step evaluation,
  • e -> e' / \(e \to 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.

5. 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

Unicode-Form:

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

LaTeX-Form:

\[
\frac{
  \Gamma \vdash e_1 : \mathrm{Num}
  \qquad
  \Gamma \vdash e_2 : \mathrm{Num}
}{
  \Gamma \vdash e_1 + e_2 : \mathrm{Num}
}
\]

Gerendert:

\[ \frac{ \Gamma \vdash e_1 : \mathrm{Num} \qquad \Gamma \vdash e_2 : \mathrm{Num} }{ \Gamma \vdash e_1 + e_2 : \mathrm{Num} } \]

Lesart:

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

5.1 Terminologie

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

Die Begriffe „Zähler/Nenner" o.ä. sind unzulässig. Bei LaTeX wird technisch zwar \frac{...}{...} verwendet, aber im Text bleibt die Regelterminologie: Prämissen und Konklusion. Der Bruchstrich ist Darstellung, keine neue Metaphysik.

5.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.

6. 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,
  • Context-Satisfaction,
  • Namespace-/Scope-Regeln,
  • 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.

7. Stilregeln

7.1 Wenige Urteilsformen, viele Anwendungen

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

7.2 Keine Symbolakrobatik

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

7.3 JDL-Code bleibt JDL-Code

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

7.4 ASCII zuerst, wenn es den Schreibfluss verbessert

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

7.5 LaTeX sparsam verwenden

LaTeX soll dort verwendet werden, wo es eine Regel sichtbar lesbarer macht: Inferenzregeln, längere Typurteile, Dependency-Urteile und verschachtelte Prämissen.

Für kurze Inline-Aussagen ist ASCII oft besser:

Gamma |- e : T

statt überall:

\(\Gamma \vdash e : T\)

Die Source-Datei soll wartbar bleiben. Git-Diffs sind kein Ort für rituelle Backslash-Opfergaben.

7.6 Formale Regel plus Lesesatz

Wichtige formale Regeln sollen durch einen kurzen Lesesatz begleitet werden.

7.7 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.8 JDL-Context nie mit Gamma gleichsetzen

In formalen Regeln gilt:

Gamma.ctx

bezeichnet den aktuellen JDL-Context.

Gamma

bezeichnet den vollständigen formalen Urteilskontext.

Diese Begriffe sind nicht austauschbar.

8. Minimale Beispielmenge

8.1 Literal-Regel

ASCII:

Gamma |- 42 : i32

LaTeX:

\[ \Gamma \vdash 42 : \mathsf{i32} \]

Lesart: 42 hat den Typ i32.

8.2 Variablenregel

ASCII:

x : T in Gamma.scope
--------------------
Gamma |- x : T

LaTeX:

\[ \frac{x : T \in \Gamma.\mathsf{scope}}{\Gamma \vdash x : T} \]

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

8.3 Additionsregel

ASCII:

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

LaTeX:

\[ \frac{ \Gamma \vdash e_1 : \mathrm{Num} \qquad \Gamma \vdash e_2 : \mathrm{Num} }{ \Gamma \vdash e_1 + e_2 : \mathrm{Num} } \]

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

8.4 Label-Erfüllung

ASCII:

Closure(T) |= Copyable

LaTeX:

\[ \mathsf{Closure}(T) \vDash \mathsf{Copyable} \]

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

8.5 Coherence-Zulässigkeit

ASCII:

Gamma |- provide P for T ok

LaTeX:

\[ \Gamma \vdash \mathsf{provide}\ P\ \mathsf{for}\ T\ \mathsf{ok} \]

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

8.6 Effect-Ausführung

ASCII:

Gamma |- eff : Effect[R, E, D]
Gamma.ctx |= D
-----------------------------
Gamma |- run(eff) : Result[R, E]

LaTeX:

\[ \frac{ \Gamma \vdash \mathit{eff} : \mathsf{Effect}[R, E, D] \qquad \Gamma.\mathsf{ctx} \vDash D }{ \Gamma \vdash \mathsf{run}(\mathit{eff}) : \mathsf{Result}[R, E] } \]

Lesart: Ein Effect darf ausgeführt werden, wenn der aktuelle JDL-Context seine Dependency-Row erfüllt.

8.7 Namespace-Auflösung

ASCII:

s resolves to q in Gamma.ns
q : T in Gamma.types
------------------------
Gamma |- s : T

LaTeX:

\[ \frac{ s \rightsquigarrow q \in \Gamma.\mathsf{ns} \qquad q : T \in \Gamma.\mathsf{types} }{ \Gamma \vdash s : T } \]

Lesart: Ein Symbol wird zuerst über die Namespace-Umgebung aufgelöst und dann über die TypeEnvironment typisiert.

9. 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.

10. 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?
  5. Wird Gamma nicht versehentlich mit JDL-context verwechselt?
  6. Sind Namespace, Scope und Context nur dann getrennt ausgeschrieben, wenn die Regel diese Trennung wirklich braucht?
  7. Ist LaTeX hier hilfreiche Renderform oder nur akademische Tapete?

Nur wenn diese Fragen sauber beantwortet werden können, sollte formale Notation verwendet werden.

11. Kurzfassung

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

Die wichtigsten ASCII-Formen sind:

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

Die wichtigsten LaTeX-Formen sind:

  • \Gamma \vdash e : T
  • \Gamma \vdash T\ \mathsf{ok}
  • \Gamma \vdash \mathsf{provide}\ P\ \mathsf{for}\ T\ \mathsf{ok}
  • \mathsf{Closure}(T) \vDash L
  • \Gamma.\mathsf{ctx} \vDash D

Zusätzlich gilt:

  • Gamma ist der formale Urteilskontext.
  • Gamma.ctx bezeichnet den aktuellen JDL-Context innerhalb dieses Urteilskontexts.
  • Gamma.scope bezeichnet lokale Bindungen.
  • Gamma.ns bezeichnet Namespace-Auflösung.
  • Gamma.types bezeichnet bekannte TypeDescriptors / die TypeEnvironment.
  • Gamma.labels bezeichnet Label-/Closure-Annahmen.

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