rev/mpl
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

Sync all reference docs with the grammar

Browse source 
- precedence.csv regenerated to the actual 14-level chain (postfix and
  prefix levels, guarded alternatives, definition vs assignment)
- glyph-escapes.md regenerated from the lexer: 73 glyphs, exactly one
  ASCII escape each, verified code points; M1-deferred symbols listed
  separately; add \middot so every glyph has an escape
- math_prog_lang.md: M0/M1 symbol split, canonical handler arrow, one-role
  semicolon, real precedence table and brace-disambiguation rules; the ten
  example programs are now embedded verbatim and CI-parsed
- Whitepaper (md + tex + appendices): every mpl code block parses or is
  re-fenced as an explicitly-labelled M1+ design sketch; symbol tables
  replaced by a pointer to glyph-escapes.md; unbuilt tooling and unmeasured
  claims reworded as planned/envisioned
- docs/ARCHITECTURE.md: status preamble, real grammar excerpt, planned
  sections labelled as such
- DocumentationTest now also covers math_prog_lang.md and the whitepaper
- CHANGELOG and DECISIONS.md updated
This commit is contained in:
developtheweb 2026-07-09 03:19:43 -04:00
parent 96002ec1bf
commit 468a8045c7
14 changed files with 558 additions and 589 deletions
Download patch file Download diff file Expand all files Collapse all files

32
CHANGELOG.md
View file

@ -8,18 +8,36 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0
## [Unreleased] ## [Unreleased]
### Added ### Added
- Comprehensive enterprise-level documentation structure - Gradle wrapper, so `./gradlew build` works from a fresh clone
- AGPLv3 license for strong copyleft protection - CI workflow: grammar build (ANTLR warnings are errors), tests, example parsing
- Complete contribution guidelines with Fatima Test emphasis - Documentation test: every ```mpl code block in README, spec and whitepaper must parse
- Security policy for vulnerability reporting - Canonical call syntax `f(a, b)` with nullary calls `f()`
- Code of conduct emphasizing language inclusivity - Wired-in operators: `≜` definition, `⊕`/`⊖` postfix resources, `⇀_ch`/`↽_ch` channels, `‧` module access, unary minus, `/` as ASCII alias of `÷`
- Enhanced .gitignore for comprehensive coverage - DECISIONS.md recording each design resolution with rejected alternatives
### Changed ### Changed
- One canonical form per construct: guarded alternatives `(c ⟹ r) | fallback`, `✎` output, `↯pattern ⟹ expr` handler clauses, exactly one ASCII escape per glyph
- `;` has a single role (sequence separator, trailing permitted)
- Identifiers may no longer start with `_`, so subscripts lex correctly
- precedence.csv and glyph-escapes.md regenerated to match the grammar exactly
- README claims reduced to what CI verifies
- Comprehensive enterprise-level documentation structure
- AGPLv3 license for strong copyleft protection (changed from MIT)
- README transformed into moonshot vision document emphasizing cognitive justice - README transformed into moonshot vision document emphasizing cognitive justice
- License changed from MIT to AGPLv3 for community protection
- Whitepaper updated to v2.0 with educational narrative focus - Whitepaper updated to v2.0 with educational narrative focus
### Fixed
- Grammar compiles: removed mutual left recursion (errors 119/148) and shadowed tokens (warning 184)
- Generated parser package no longer declared twice
- Gradle finds the grammar (src/main/antlr4) and the ParseExamples main class
- Test harness uses CharStreams; supplementary-plane glyphs (𝔹, 𝓜, 🖫) now tokenize
- Examples 03 and 05 parse (canonical handler arrow; real placeholder body)
### Removed
- Dead tokens with no parser rule: `?` (QUERY), `∃`, `⇐`, `→`, `.`
- Juxtaposition function application (`f x`)
- C-style ternary and `📤` from all documentation
## [2.0.0] - 2025-01-26 ## [2.0.0] - 2025-01-26
### Added ### Added

3
DECISIONS.md
View file

@ -27,3 +27,6 @@ against the existing examples.
- **Exactly one ASCII escape per glyph** (`\lambda` not `\lam`, `\leftarrow` not `\gets`, `\neq` not `\ne`, `\nat` not `\N`, …); rejected: alias sets (two ways to write the same token). - **Exactly one ASCII escape per glyph** (`\lambda` not `\lam`, `\leftarrow` not `\gets`, `\neq` not `\ne`, `\nat` not `\N`, …); rejected: alias sets (two ways to write the same token).
- **`%` (modulo), `∑`, `√`, `²`, `|x|`, ranges `[a..b]`, indexing/slicing, `where`, and record field access are NOT in M0** — every document says so instead of using them; deferred to M1 with semantics, not smuggled in via prose. - **`%` (modulo), `∑`, `√`, `²`, `|x|`, ranges `[a..b]`, indexing/slicing, `where`, and record field access are NOT in M0** — every document says so instead of using them; deferred to M1 with semantics, not smuggled in via prose.
- **Lambda parameters are a bare comma-separated pattern list** (`λa, b: body`); rejected: parenthesized parameter lists `λ(a, b):` (two ways to write parameters). - **Lambda parameters are a bare comma-separated pattern list** (`λa, b: body`); rejected: parenthesized parameter lists `λ(a, b):` (two ways to write parameters).
- **`‧` gets the escape `\middot`** so the "every glyph has an ASCII escape" claim stays true; rejected: leaving MIDDOT as the one escape-less glyph.
- **`glyph-escapes.md` and `precedence.csv` are the only symbol/precedence tables**; the whitepaper appendix points at them instead of duplicating them; rejected: parallel tables that drift (the old appendix disagreed with the lexer on several code points and escapes).
- **Documentation code blocks are fenced ```mpl only if they parse today**; M1+ sketches are fenced as plain text with an explicit "not yet parseable" caption, and a CI test enforces the rule for README, spec, and whitepaper.

68
docs/ARCHITECTURE.md
View file

@ -2,6 +2,11 @@
This document describes the high-level architecture of the Mathematical Programming Language (MPL) implementation. This document describes the high-level architecture of the Mathematical Programming Language (MPL) implementation.
**Status**: only the lexing and parsing layers exist today (see the README's
project status). Everything from semantic analysis down — and the runtime,
error-message, performance and security sections below — describes the
*target* architecture, not shipped code.
## Overview ## Overview
MPL is designed as a multi-layer system that transforms mathematical notation into executable code: MPL is designed as a multi-layer system that transforms mathematical notation into executable code:
@ -60,22 +65,22 @@ MPL is designed as a multi-layer system that transforms mathematical notation in
### 1. Grammar Definition (`src/main/antlr4/MPL.g4`) ### 1. Grammar Definition (`src/main/antlr4/MPL.g4`)
The heart of MPL is its ANTLR 4 grammar that defines: The heart of MPL is its ANTLR 4 grammar that defines:
- **70+ Mathematical Operators**: From basic arithmetic to advanced calculus - **Mathematical Operators**: every glyph with exactly one meaning and one ASCII escape ([glyph-escapes.md](../glyph-escapes.md))
- **Effect Operators**: Exception handling (↯/↴), concurrency (‖), resources (⊕/⊖) - **Effect Operators**: Exception handling (↯/↴), concurrency (‖), resources (⊕/⊖)
- **Precedence Rules**: Mathematically consistent operator precedence - **Precedence Rules**: a documented chain ([precedence.csv](../precedence.csv))
- **Zero Conflicts**: No shift/reduce or reduce/reduce conflicts - **CI-clean**: compiles with zero ANTLR errors and warnings (`-Werror`)
Key grammar features: Key grammar rules (excerpted from the real grammar):
```antlr ```antlr
// Example: Function definition // Definition and assignment levels of the precedence chain
functionDef : name=IDENTIFIER '≜' lambda ; defExpr : assignExpr (DEFINITION defExpr)? ; // x ≜ e
lambda : 'λ' params ':' expression ; assignExpr : condExpr (LEFTARROW assignExpr)? ; // x ← e
// Example: Mathematical operations // Guarded alternatives: (condition ⟹ result) | fallback
expression : expression '×' expression # Multiplication condExpr : impliesExpr (BAR impliesExpr)* ;
| expression '÷' expression # Division
| '∑' '(' var '∈' range ':' expression ')' # Summation // λx: body, λx,y: body, λx∈ℝ: body
; lambda : LAMBDA_VAR pattern (IN condExpr)? COLON expr ;
``` ```
### 2. Symbol System ### 2. Symbol System
@ -83,21 +88,20 @@ expression : expression '×' expression # Multiplication
MPL uses a three-tier symbol system: MPL uses a three-tier symbol system:
1. **Unicode Symbols** (Primary) 1. **Unicode Symbols** (Primary)
- Direct mathematical notation: ∀, ∃, λ, ∑, ∏ - Direct mathematical notation: ∀, λ, ∈, ⟹
- Effect operators: ↯, ↴, ‖, ⇀, ↽ - Effect operators: ↯, ↴, ‖, ⇀, ↽
- Type symbols: ℕ, ℤ, ℝ, ℂ, 𝔹 - Type symbols: ℕ, ℤ, ℚ, ℝ, ℂ, 𝔹
2. **ASCII Escapes** (Fallback) 2. **ASCII Escapes** (Fallback)
- Every symbol has an escape: `\forall`, `\lambda`, `\sum` - Every symbol has exactly one escape: `\forall`, `\lambda`, …
- Bidirectional conversion supported - Defined in `glyph-escapes.md` (kept in lockstep with the lexer)
- Defined in `glyph-escapes.md`
3. **Multi-Modal Input** (Future) 3. **Multi-Modal Input** (Future)
- Voice recognition for mathematical terms - Voice recognition for mathematical terms
- Visual palette selection - Visual palette selection
- Handwriting recognition - Handwriting recognition
### 3. Type System ### 3. Type System (planned, M1)
MPL features a hybrid type system: MPL features a hybrid type system:
@ -146,7 +150,7 @@ MPLVisitor visitor = new MPLASTBuilder();
AST ast = visitor.visit(tree); AST ast = visitor.visit(tree);
``` ```
### 6. Runtime Architecture ### 6. Runtime Architecture (planned)
The MPL runtime provides: The MPL runtime provides:
@ -180,43 +184,43 @@ The MPL runtime provides:
3. AST construction 3. AST construction
4. Syntax error recovery 4. Syntax error recovery
### Phase 3: Semantic Analysis ### Phase 3: Semantic Analysis (planned)
1. Symbol table construction 1. Symbol table construction
2. Type inference 2. Type inference
3. Effect analysis 3. Effect analysis
4. Semantic error checking 4. Semantic error checking
### Phase 4: Optimization ### Phase 4: Optimization (planned)
1. Constant folding 1. Constant folding
2. Common subexpression elimination 2. Common subexpression elimination
3. Parallelism detection 3. Parallelism detection
4. Effect optimization 4. Effect optimization
### Phase 5: Code Generation ### Phase 5: Code Generation (planned)
Options for different targets: Options for different targets:
- **JVM Bytecode**: For Java interoperability - **JVM Bytecode**: For Java interoperability
- **LLVM IR**: For native compilation - **LLVM IR**: For native compilation
- **JavaScript**: For web execution - **JavaScript**: For web execution
- **Python**: For educational use - **Python**: For educational use
## Error Handling ## Error Handling (planned)
MPL provides comprehensive error messages with: Today the parser emits standard ANTLR diagnostics. The goal is comprehensive error messages with:
1. **Unicode-aware positioning**: Correct column numbers for multi-byte characters 1. **Unicode-aware positioning**: Correct column numbers for multi-byte characters
2. **Multi-language messages**: Errors in user's native language 2. **Multi-language messages**: Errors in user's native language
3. **Visual error display**: Highlighting problematic symbols 3. **Visual error display**: Highlighting problematic symbols
4. **Suggestion system**: Common fixes for typical mistakes 4. **Suggestion system**: Common fixes for typical mistakes
Example error: Envisioned example error:
``` ```
Error at line 3, column 15: Error at line 3, column 12:
∑(i ∈ [1,10] : i²²) (x > 0 ⟹ x | -x
^^ ^
Syntax error: Unexpected ² after ² Syntax error: missing ')' before '|'
Did you mean: i² × ² or i⁴? Guarded alternatives read: (condition ⟹ result) | fallback
``` ```
## Performance Considerations ## Performance Considerations (planned)
1. **Parser Performance** 1. **Parser Performance**
- O(n) parsing for most constructs - O(n) parsing for most constructs
@ -242,7 +246,7 @@ The architecture supports extensions via:
3. **Effect Extensions**: New computational effects 3. **Effect Extensions**: New computational effects
4. **Backend Extensions**: Additional compilation targets 4. **Backend Extensions**: Additional compilation targets
## Security Considerations ## Security Considerations (planned)
1. **Input Validation** 1. **Input Validation**
- Unicode homograph detection - Unicode homograph detection

146
glyph-escapes.md
View file

@ -1,10 +1,16 @@
# MPL Glyph Escape Sequences # MPL Glyph Escape Sequences
This document provides the authoritative mapping between ASCII escape sequences and UTF-8 glyphs for the Mathematical Programming Language (MPL). This document is the authoritative mapping between ASCII escape sequences and
UTF-8 glyphs for the Mathematical Programming Language (MPL). It matches the
lexer rules in [`src/main/antlr4/MPL.g4`](src/main/antlr4/MPL.g4) exactly:
every escape below is accepted by the lexer, and no other escapes exist.
## Core Mathematical Symbols Each glyph has **exactly one** ASCII escape (One Right Answer). Symbols that
are plain ASCII (`; = < > + - ( ) [ ] { } : , _ | /` and the keywords
`true`/`false`) need no escape and have none.
## Greek Letters (Variables)
### Greek Letters (Variables)
| ASCII Escape | Unicode | Glyph | Usage | | ASCII Escape | Unicode | Glyph | Usage |
|-------------|---------|-------|-------| |-------------|---------|-------|-------|
| `\alpha` | U+03B1 | α | Variable | | `\alpha` | U+03B1 | α | Variable |
@ -17,12 +23,12 @@ This document provides the authoritative mapping between ASCII escape sequences
| `\theta` | U+03B8 | θ | Variable | | `\theta` | U+03B8 | θ | Variable |
| `\iota` | U+03B9 | ι | Variable | | `\iota` | U+03B9 | ι | Variable |
| `\kappa` | U+03BA | κ | Variable | | `\kappa` | U+03BA | κ | Variable |
| `\lambda` or `\lam` | U+03BB | λ | Lambda/Function | | `\lambda` | U+03BB | λ | Lambda / variable |
| `\mu` | U+03BC | μ | Variable | | `\mu` | U+03BC | μ | Variable |
| `\nu` | U+03BD | ν | Variable | | `\nu` | U+03BD | ν | Variable |
| `\xi` | U+03BE | ξ | Variable | | `\xi` | U+03BE | ξ | Variable |
| `\omicron` | U+03BF | ο | Variable | | `\omicron` | U+03BF | ο | Variable |
| `\pi` | U+03C0 | π | Variable/Constant | | `\pi` | U+03C0 | π | Variable |
| `\rho` | U+03C1 | ρ | Variable | | `\rho` | U+03C1 | ρ | Variable |
| `\sigma` | U+03C3 | σ | Variable | | `\sigma` | U+03C3 | σ | Variable |
| `\tau` | U+03C4 | τ | Variable | | `\tau` | U+03C4 | τ | Variable |
@ -32,110 +38,94 @@ This document provides the authoritative mapping between ASCII escape sequences
| `\psi` | U+03C8 | ψ | Variable | | `\psi` | U+03C8 | ψ | Variable |
| `\omega` | U+03C9 | ω | Variable | | `\omega` | U+03C9 | ω | Variable |
### Set Theory ## Type Symbols
| ASCII Escape | Unicode | Glyph | Usage |
|-------------|---------|-------|-------|
| `\nat` | U+2115 | ℕ | Natural numbers |
| `\int` | U+2124 | ℤ | Integers |
| `\rat` | U+211A | ℚ | Rational numbers |
| `\real` | U+211D | ℝ | Real numbers |
| `\complex` | U+2102 | ℂ | Complex numbers |
| `\bool` | U+1D539 | 𝔹 | Booleans |
| `\bot` | U+22A5 | ⊥ | Bottom |
## Logic and Sets
| ASCII Escape | Unicode | Glyph | Usage | | ASCII Escape | Unicode | Glyph | Usage |
|-------------|---------|-------|-------| |-------------|---------|-------|-------|
| `\emptyset` | U+2205 | ∅ | Empty set |
| `\union` or `\cup` | U+222A | ∪ | Set union |
| `\intersect` or `\cap` | U+2229 | ∩ | Set intersection |
| `\subset` | U+2282 | ⊂ | Proper subset |
| `\supset` | U+2283 | ⊃ | Proper superset |
| `\in` | U+2208 | ∈ | Element of | | `\in` | U+2208 | ∈ | Element of |
| `\notin` | U+2209 | ∉ | Not element of | | `\emptyset` | U+2205 | ∅ | Empty set |
| `\subseteq` | U+2286 | ⊆ | Subset or equal | | `\and` | U+2227 | ∧ | Logical and |
| `\supseteq` | U+2287 | ⊇ | Superset or equal | | `\or` | U+2228 | ∨ | Logical or |
| `\implies` | U+27F9 | ⟹ | Implication / guard arrow |
| `\forall` | U+2200 | ∀ | Universal quantifier (iteration) |
### Logic ## Operations
| ASCII Escape | Unicode | Glyph | Usage |
|-------------|---------|-------|-------|
| `\and` or `\wedge` | U+2227 | ∧ | Logical and |
| `\or` or `\vee` | U+2228 | ∨ | Logical or |
| `\not` or `\neg` | U+00AC | ¬ | Logical not |
| `\implies` or `\Rightarrow` | U+27F9 | ⟹ | Implication |
| `\iff` or `\Leftrightarrow` | U+27FA | ⟺ | If and only if |
| `\forall` | U+2200 | ∀ | Universal quantifier |
| `\exists` | U+2203 | ∃ | Existential quantifier |
### Operations
| ASCII Escape | Unicode | Glyph | Usage | | ASCII Escape | Unicode | Glyph | Usage |
|-------------|---------|-------|-------| |-------------|---------|-------|-------|
| `\times` | U+00D7 | × | Multiplication | | `\times` | U+00D7 | × | Multiplication |
| `\div` | U+00F7 | ÷ | Division | | `\div` | U+00F7 | ÷ | Division (`/` is an ASCII alias) |
| `\ast` | U+2217 | ∗ | Generic operator | | `\ast` | U+2217 | ∗ | Generic operator |
| `\circ` | U+2218 | ∘ | Function composition | | `\circ` | U+2218 | ∘ | Function composition |
### Relations ## Relations
| ASCII Escape | Unicode | Glyph | Usage | | ASCII Escape | Unicode | Glyph | Usage |
|-------------|---------|-------|-------| |-------------|---------|-------|-------|
| `\neq` or `\ne` | U+2260 | ≠ | Not equal | | `\neq` | U+2260 | ≠ | Not equal |
| `\leq` or `\le` | U+2264 | ≤ | Less than or equal | | `\leq` | U+2264 | ≤ | Less than or equal |
| `\geq` or `\ge` | U+2265 | ≥ | Greater than or equal | | `\geq` | U+2265 | ≥ | Greater than or equal |
| `\approx` | U+2248 | ≈ | Approximately equal | | `\approx` | U+2248 | ≈ | Approximately equal |
| `\sim` | U+223C | ∼ | Similar to | | `\sim` | U+223C | ∼ | Similar to |
### Special Symbols ## Definition and Assignment
| ASCII Escape | Unicode | Glyph | Usage | | ASCII Escape | Unicode | Glyph | Usage |
|-------------|---------|-------|-------| |-------------|---------|-------|-------|
| `\leftarrow` or `\gets` | U+2190 | ← | Assignment | | `\leftarrow` | U+2190 | ← | Assignment |
| `\coloneq` | U+225C | ≜ | Definition | | `\coloneq` | U+225C | ≜ | Definition |
| `\rightarrow` or `\to` | U+2192 | → | Function type |
## Effect Extensions ## Effect Operators
| ASCII Escape | Unicode | Glyph | Usage | | ASCII Escape | Unicode | Glyph | Usage |
|-------------|---------|-------|-------| |-------------|---------|-------|-------|
| `\raise` | U+21AF | ↯ | Raise exception | | `\raise` | U+21AF | ↯ | Raise exception |
| `\handle` | U+21B4 | ↴ | Handle exception | | `\handle` | U+21B4 | ↴ | Handle exception (postfix) |
| `\parallel` | U+2016 | ‖ | Parallel composition | | `\parallel` | U+2016 | ‖ | Parallel composition |
| `\lceil` | U+2308 | ⌈ | Atomic section start | | `\lceil` | U+2308 | ⌈ | Atomic section start |
| `\rceil` | U+2309 | ⌉ | Atomic section end | | `\rceil` | U+2309 | ⌉ | Atomic section end |
| `\oplus` | U+2295 | ⊕ | Allocate resource | | `\oplus` | U+2295 | ⊕ | Allocate resource (postfix) |
| `\ominus` | U+2296 | ⊖ | Release resource | | `\ominus` | U+2296 | ⊖ | Release resource (postfix) |
| `\module` | U+1D49C | 𝓜 | Module declaration | | `\send` | U+21C0 | ⇀ | Send to channel: `⇀_ch expr` |
| `\Leftarrow` | U+21D0 | ⇐ | Import | | `\receive` | U+21BD | ↽ | Receive from channel: `↽_ch expr` |
| `\Rightarrow` | U+21D2 | ⇒ | Export | | `\trace` | U+270E | ✎ | Output / trace |
| `\send` | U+21C0 | ⇀ | Send (network) | | `\break` | U+29C8 | ⧈ | Breakpoint |
| `\receive` | U+21BD | ↽ | Receive (network) | | `\delay` | U+23F2 | ⏲ | Delay |
| `\periodic` | U+27F3 | ⟳ | Periodic task |
## Additional Operators ## Modules and Metaprogramming
| ASCII Escape | Unicode | Glyph | Usage | | ASCII Escape | Unicode | Glyph | Usage |
|-------------|---------|-------|-------| |-------------|---------|-------|-------|
| `\langle` | U+27E8 | ⟨ | Choice type/angle bracket left | | `\module` | U+1D4DC | 𝓜 | Module declaration |
| `\rangle` | U+27E9 | ⟩ | Choice type/angle bracket right | | `\Rightarrow` | U+21D2 | ⇒ | Export (module body follows) |
| `\middot` | U+2027 | ‧ | Qualified module access |
| `\path` | U+1F5AB | 🖫 | File path prefix | | `\path` | U+1F5AB | 🖫 | File path prefix |
| `\up` | U+21E1 | ⇡ | Stream position up |
| `\down` | U+21E3 | ⇣ | Stream position down |
| `\swap` | U+21C6 | ⇆ | Atomic swap |
| `\llangle` | U+27EA | ⟪ | Deep update path start |
| `\rrangle` | U+27EB | ⟫ | Deep update path end |
| `\ulcorner` | U+231C | ⌜ | Code quotation start | | `\ulcorner` | U+231C | ⌜ | Code quotation start |
| `\urcorner` | U+231D | ⌝ | Code quotation end | | `\urcorner` | U+231D | ⌝ | Code quotation end |
| `\llcorner` | U+231E | ⌞ | Code evaluation start | | `\llcorner` | U+231E | ⌞ | Code evaluation start |
| `\lrcorner` | U+231F | ⌟ | Code evaluation end | | `\lrcorner` | U+231F | ⌟ | Code evaluation end |
| `\query` | U+003F | ? | Introspection |
| `\break` | U+2A08 | ⧈ | Breakpoint |
| `\trace` | U+270E | ✎ | Trace/log |
| `\delay` | U+23F2 | ⏲ | Delay |
| `\periodic` | U+27F3 | ⟳ | Periodic task |
| `\lbracket` | U+3014 | 〔 | RAII scope start | | `\lbracket` | U+3014 | 〔 | RAII scope start |
| `\rbracket` | U+3015 | 〕 | RAII scope end | | `\rbracket` | U+3015 | 〕 | RAII scope end |
| `\langle` | U+27E8 | ⟨ | Choice type start |
## Type System Symbols | `\rangle` | U+27E9 | ⟩ | Choice type end |
| ASCII Escape | Unicode | Glyph | Usage |
|-------------|---------|-------|-------|
| `\nat` or `\N` | U+2115 | ℕ | Natural numbers |
| `\int` or `\Z` | U+2124 | ℤ | Integers |
| `\rat` or `\Q` | U+211A | ℚ | Rational numbers |
| `\real` or `\R` | U+211D | ℝ | Real numbers |
| `\complex` or `\C` | U+2102 | ℂ | Complex numbers |
| `\bool` or `\B` | U+1D539 | 𝔹 | Booleans |
| `\bot` | U+22A5 | ⊥ | Bottom type |
## String Escape Sequences ## String Escape Sequences
String literals in MPL support the following escape sequences within double-quoted strings: String literals in MPL support the following escape sequences within
double-quoted strings:
| Escape Sequence | Character | Description | | Escape Sequence | Character | Description |
|----------------|-----------|-------------| |----------------|-----------|-------------|
@ -153,18 +143,20 @@ Examples:
- `"Unicode: \u{1F600}"` - Unicode emoji 😀 - `"Unicode: \u{1F600}"` - Unicode emoji 😀
- `"""Raw string - no \n escapes"""` - Raw multi-line string - `"""Raw string - no \n escapes"""` - Raw multi-line string
## Deferred to M1
The following glyphs appeared in earlier drafts but are **not** part of the
M0 grammar. Each returns only together with a defined semantic:
∪ ∩ ⊂ ⊃ ⊆ ⊇ ∉ ¬ ⟺ ∃ ⇐ → ⇡ ⇣ ⇆ ⟪ ⟫ ∑ √ ² `?` `%`
## Usage Notes ## Usage Notes
1. **Input methods:** 1. **Input methods:**
- Direct Unicode input (recommended for supported editors) - Direct Unicode input (recommended for supported editors)
- ASCII escape sequences (for compatibility) - ASCII escape sequences (for compatibility, work in any editor)
- Editor-specific shortcuts (e.g., Ctrl+Alt+g → γ)
2. **Lexer behavior:** 2. **Lexer behavior:**
- Escapes are processed during tokenization - Escapes are alternatives in the lexer rules, processed during tokenization
- Unknown escapes result in compilation error - Unknown escapes are a lexical error
- Mixed Unicode/ASCII in same file is allowed - Mixed Unicode/ASCII in the same file is allowed
3. **Pretty-printing:**
- Always outputs Unicode glyphs (never escapes)
- Configurable fallback to ASCII for terminals without Unicode support

231
math_prog_lang.md
View file

@ -1,180 +1,204 @@
# Mathematical Programming Language (MPL) # Mathematical Programming Language (MPL)
## Core Symbol Set This is the language specification. The single source of truth for what
parses is the grammar, [`src/main/antlr4/MPL.g4`](src/main/antlr4/MPL.g4);
every symbol and example below is part of the M0 grammar unless explicitly
marked "M1".
## Core Symbol Set (M0)
### Mathematical Foundation (LaTeX) ### Mathematical Foundation (LaTeX)
- **Variables:** α,β,γ,δ,ε,ζ,η,θ,ι,κ,λ,μ,ν,ξ,ο,π,ρ,σ,τ,υ,φ,χ,ψ,ω - **Variables:** α,β,γ,δ,ε,ζ,η,θ,ι,κ,λ,μ,ν,ξ,ο,π,ρ,σ,τ,υ,φ,χ,ψ,ω
- **Collections:** ∅,∪,∩,⊂,⊃,∈,∉,⊆,⊇ - **Collections:** ∅,∈
- **Logic:** ∧,∨,¬,⟹,⟺,∀,∃ - **Logic:** ∧,∨,⟹,∀
- **Operations:** +,-,×,÷,∗,∘ - **Operations:** +,-,×,÷ (ASCII alias `/`),∗,∘
- **Relations:** =,≠,<,>,≤,≥,≈,∼ - **Relations:** =,≠,<,>,≤,≥,≈,∼
- **Functions:** f: A → B, λ - **Functions:** λ (calls are `f(a, b)`)
- **Assignment:** ← - **Assignment:** ←
- **Definition:** ≜ - **Definition:** ≜
- **Structure:** (),[],{},⟨⟩ - **Structure:** (),[],{},⟨⟩
### Effect Extensions (11 new glyphs) ### Effect Extensions
- **↯** Raise exception - **↯** Raise exception
- **↴** Handle exception - **↴** Handle exception (postfix: `expr ↴ { ↯pattern ⟹ expr }`)
- **‖** Parallel composition - **‖** Parallel composition
- **⌈⌉** Atomic section/lock - **⌈⌉** Atomic section/lock (optional subscript: `⌈…⌉_lock`)
- **⊕** Allocate resource - **⊕** Allocate resource (postfix: `database ⊕`)
- **⊖** Release resource - **⊖** Release resource (postfix: `conn ⊖`)
- **𝓜** Module declaration - **𝓜** Module declaration
- **⇐** Import
- **⇒** Export - **⇒** Export
- **⇀** Send (network) - **‧** Qualified module access (`Mathematics‧sin`)
- **↽** Receive (network) - **⇀** Send to channel (`⇀_ch expr`)
- **↽** Receive from channel (`↽_ch expr`)
### Additional Operators ### Additional Operators
- **⟨v|e⟩** Choice type (value or error) - **⟨v|e⟩** Choice type (value or error)
- **🖫** File path prefix - **🖫** File path prefix (`🖫"file.txt"` or `🖫identifier`)
- **⇡⇣** Stream positioning
- **⇆** Atomic swap
- **⟪⟫** Deep update path
- **⌜⌝** Code quotation - **⌜⌝** Code quotation
- **⌞⌟** Code evaluation - **⌞⌟** Code evaluation
- **?** Introspection
- **⧈** Breakpoint - **⧈** Breakpoint
- **✎** Trace/log - **✎** Trace/log (the one output operator)
- **⏲** Delay - **⏲** Delay
- **⟳** Periodic task - **⟳** Periodic task
- **〔〕** RAII scope - **〔〕** RAII scope
### Reserved for M1 (not in the grammar)
∪,∩,⊂,⊃,⊆,⊇,∉ (set algebra); ¬,⟺,∃ (extended logic); → (function
types); ⇐ (import); ⇡⇣ (stream positioning); ⇆ (atomic swap); ⟪⟫ (deep
update); ? (introspection); ∑,√,²,% (arithmetic extensions). Each returns
only together with a defined semantic.
## Grammar ## Grammar
The sketches below are illustrative; [`MPL.g4`](src/main/antlr4/MPL.g4) is
normative.
### Basic Expressions ### Basic Expressions
``` ```
expr ::= variable | literal | operation | function_call | block expr ::= variable | literal | operation | function_call | block
variable ::= α | β | γ | ... | ω variable ::= identifier | α | β | γ | ... | ω
literal ::= number | string | path | list | set literal ::= number | string | path | list | set | record
operation ::= expr OP expr operation ::= expr OP expr
function_call ::= f(expr, ...) function_call ::= f(expr, ...) -- the one call syntax; f() is legal
block ::= { statement; ... } block ::= { expr; expr; ... } -- ; separates, trailing ; permitted
``` ```
### Statements ### Expression Forms
``` ```
assignment ::= variable ← expr assignment ::= expr ← expr
definition ::= variable ≜ expr definition ::= expr ≜ expr
conditional ::= condition ⟹ expr conditional ::= (condition ⟹ result) | fallback -- guarded alternatives
iteration ::= ∀variable∈set: expr iteration ::= ∀pattern∈domain: expr
lambda ::= λpattern: expr | λpattern∈domain: expr
parallel ::= expr ‖ expr parallel ::= expr ‖ expr
atomic ::= ⌈expr⌉_lock atomic ::= ⌈expr⌉ | ⌈expr⌉_lock
exception ::= ↯expr | expr ↴ {↯e ⇒ handler} exception ::= ↯expr | expr ↴ {↯pattern ⟹ handler; ...}
``` ```
### Types ### Types
``` ```
basic_type ::= ℕ | ℤ | ℚ | ℝ | ℂ | 𝔹 basic_type ::= ℕ | ℤ | ℚ | ℝ | ℂ | 𝔹
function_type ::= domain → codomain
choice_type ::= ⟨type|type⟩ choice_type ::= ⟨type|type⟩
effect_type ::= type^effect function_type ::= domain → codomain -- M1
effect_type ::= type^effect -- M1
``` ```
## Example Programs ## Example Programs
These are the ten programs in [`examples/`](examples/), verbatim; CI parses
them on every push (`./gradlew parseExamples`).
### Hello World ### Hello World
``` ```mpl
✎"Hello, World!" -- Hello World example
✎"Hello, World!";
``` ```
### Factorial ### Factorial
``` ```mpl
factorial ≜ λn∈ℕ: n≤1 ⟹ 1 | n×factorial(n-1) -- Factorial example with proper precedence
result ← factorial(5) factorial ≜ λn∈ℕ: (n≤1 ⟹ 1) | (n×factorial(n-1));
✎result result ← factorial(5);
✎result;
``` ```
### File Processing with Error Handling ### File Processing with Error Handling
``` ```mpl
processFile ≜ λpath: 🖫path ↴ { -- File processing with error handling
data ← readFile(path) processFile ≜ λpath: {
result ← transform(data) data ← readFile(🖫path);
writeFile(result, 🖫"output.txt") result ← transform(data);
writeFile(result, 🖫"output.txt");
⟨"success"|"failed"⟩ ⟨"success"|"failed"⟩
} ↴ {↯e ⇒ ⟨⊥|e⟩} } ↴ {↯e ⟹ ⟨⊥|e⟩};
``` ```
### Concurrent Download ### Concurrent Download
``` ```mpl
-- Concurrent download with parallelism
downloadAll ≜ λurls: ∀url∈urls: ( downloadAll ≜ λurls: ∀url∈urls: (
fetchData(url) ‖ processData(url) fetchData(url) ‖ processData(url)
) ⟹ mergeResults() ) ⟹ mergeResults();
``` ```
### Module Definition ### Module Definition
``` ```mpl
-- Module definition example
𝓜 Mathematics ⇒ { 𝓜 Mathematics ⇒ {
π ≜ 3.14159... π ≜ 3.14159;
sin ≜ λx∈ℝ: ... sin ≜ λx∈ℝ: ⊥ {- implementation deferred until MPL executes -};
cos ≜ λx∈ℝ: ... cos ≜ λx∈ℝ: ⊥ {- implementation deferred until MPL executes -}
} };
angle ← π/4 angle ← π/4;
result ← Mathematics‧sin(angle) result ← Mathematics‧sin(angle);
``` ```
### Resource Management ### Resource Management
``` ```mpl
-- Resource management with RAII
databaseQuery ≜ λquery: 〔 databaseQuery ≜ λquery: 〔
conn ← database ⊕ conn ← database ⊕;
⌈ ⌈
result ← execute(conn, query) result ← execute(conn, query);
✎"Query executed" ✎"Query executed";
result result
⌉_db_lock ⌉_db_lock
conn ⊖ {- conn ⊖ happens automatically at end of 〔〕 -}
〕 〕;
``` ```
### Metaprogramming ### Metaprogramming
``` ```mpl
-- Metaprogramming with code quotation
generateFunction ≜ λname: ⌜ generateFunction ≜ λname: ⌜
λx: x × 2 λx: x × 2
⌝ ⌝;
doubler ← ⌞generateFunction("doubler")⌟ doubler ← ⌞generateFunction("doubler")⌟;
result ← doubler(21) result ← doubler(21);
``` ```
### Real-time System ### Real-time System
``` ```mpl
-- Real-time scheduler with periodic tasks
scheduler ≜ ⟳( scheduler ≜ ⟳(
tasks ← getPendingTasks() tasks ← getPendingTasks();
∀task∈tasks: execute(task) ‖ monitor(task) ∀task∈tasks: execute(task) ‖ monitor(task),
, 100ms 100ms
) );
``` ```
### Network Server ### Network Server
``` ```mpl
-- Network server with connection handling
server ≜ λport: 〔 server ≜ λport: 〔
socket ← bind(port) ⊕ socket ← bind(port) ⊕;
∀request: ( ∀request∈acceptLoop(socket): (
data ← ↽_socket request data ← ↽_socket request;
response ← processRequest(data) response ← processRequest(data);
⇀_socket response ⇀_socket response
) ‖ handleNext() ) ‖ handleNext()
socket ⊖ {- socket ⊖ happens automatically at end of 〔〕 -}
〕 〕;
``` ```
### Type-safe Database ### Type-safe Database
``` ```mpl
User ≜ {name: String, age: ℕ∣age>0, email: String} -- Type-safe database with refinement types
User ≜ {name: String, age: ℕ | age>0, email: String};
query ≜ λtable∈Database: ∀row∈table: validateUser(row) ↴ { query ≜ λtable∈Database: ∀row∈table: validateUser(row) ↴ {
↯"Invalid user" ⟹ ⊥ ↯"Invalid user" ⟹ ⊥
} };
``` ```
## Critical Implementation Decisions ## Critical Implementation Decisions
### Lexical Layer ### Lexical Layer
- **Unicode Normalization:** NFC on ingest, reject mixed forms - **Unicode Normalization:** NFC on ingest, reject mixed forms (planned; the parser currently consumes code points as-is)
- **Symbol Input:** Cross-platform keymap (Ctrl+Alt+g → γ) + ASCII escapes (\gamma → γ) - **Symbol Input:** ASCII escapes (\gamma → γ), exactly one per glyph; editor keymaps are future tooling
- **Semicolon handling:** Require explicit `;` everywhere except before `}` - **Semicolon handling:** `;` has one role — it separates expressions in a sequence; a trailing `;` is permitted (so `;` before `}` is legal but not required)
- **Comments:** `--` for single-line comments (to end of line), `{- ... -}` for multi-line comments (nestable) - **Comments:** `--` for single-line comments (to end of line), `{- ... -}` for multi-line comments (nestable)
- **String Literals:** - **String Literals:**
- Standard strings: `"..."` with escape sequences (`\n`, `\t`, `\\`, `\"`, `\u{XXXXXX}`) - Standard strings: `"..."` with escape sequences (`\n`, `\t`, `\\`, `\"`, `\u{XXXXXX}`)
@ -183,25 +207,31 @@ query ≜ λtable∈Database: ∀row∈table: validateUser(row) ↴ {
- **Number Literals:** Decimal (`123`, `3.14`), hex (`0x1A`), binary (`0b1101`), with optional type suffixes later - **Number Literals:** Decimal (`123`, `3.14`), hex (`0x1A`), binary (`0b1101`), with optional type suffixes later
### Operator Precedence Table ### Operator Precedence Table
Authoritative copy: [precedence.csv](precedence.csv).
| Level | Operators | Associativity | | Level | Operators | Associativity |
|-------|-----------|---------------| |-------|-----------|---------------|
| 9 | function application | left | | 11 | f(a, b) ‧ ⊕ ⊖ ↴{…} (postfix) | left |
| 8 | ↯ ✎ ? ⧈ ⏲ (prefix) | right | | 10 | ↯ ✎ ⧈ ⏲ - ⇀_ch ↽_ch (prefix) | right |
| 7 | ∘ | left | | 9 | ∘ | left |
| 6 | × ÷ ∗ | left | | 8 | × ÷ ∗ | left |
| 5 | + - | left | | 7 | + - | left |
| 4 | = ≠ < > ≤ ≥ ≈ ∼ | non-assoc | | 6 | = ≠ < > ≤ ≥ ≈ ∼ | non-assoc |
| 3 | ∧ | left | | 5 | ∧ | left |
| 2 | ∨ | left | | 4 | ∨ | left |
| 1 | ⟹ | right | | 3 | ⟹ | right |
| 0 | ← | right | | 2 | \| (guarded alternatives) | left |
| 1 | ← | right |
| 0 | ≜ | right |
| -1 | ‖ | left | | -1 | ‖ | left |
| -2 | ; | left | | -2 | ; | left |
### Grammar Resolutions ### Grammar Resolutions
- **Block semantics:** Every statement returns value (ML-style) - **Block semantics:** Every expression in a sequence yields a value (ML-style)
- **Conditional associativity:** Right-associative (a⟹b⟹c = a⟹(b⟹c)) - **Conditional associativity:** ⟹ is right-associative (a⟹b⟹c = a⟹(b⟹c)); guarded alternatives chain left: (c₁ ⟹ r₁) | (c₂ ⟹ r₂) | fallback
- **Choice type parsing:** Different tokens for |value vs |type contexts - **Choice type parsing:** one BAR token; the `|` inside ⟨a|b⟩ is the guarded-alternative level of the inner expression
- **Brace disambiguation:** `{a: e, …}` record, `{a, b, …}` set (two or more elements), anything else (incl. `{}`, `{x}`) a block
### Type System Extensions ### Type System Extensions
- **Effect polymorphism:** `map : (A→ᴱ B) → List A →ᴱ List B` - **Effect polymorphism:** `map : (A→ᴱ B) → List A →ᴱ List B`
@ -262,13 +292,16 @@ map ≜ ΛA. ΛB. λf: A→ᴱ B. λxs: List A. …
``` ```
Γ ⊢ e₁ : α Γ ⊢ e₂ : β Γ ⊢ e₃ : β Γ ⊢ e₁ : α Γ ⊢ e₂ : β Γ ⊢ e₃ : β
───────────────────────────────────────────────────────── (HANDLE) ───────────────────────────────────────────────────────── (HANDLE)
Γ ⊢ e₁ ↴ { ↯x ⇒ e₂ } : β ▷ Eff = (Eff(e₁) - {Raise ε}) ∪ Eff(e₂) Γ ⊢ e₁ ↴ { ↯x ⟹ e₂ } : β ▷ Eff = (Eff(e₁) - {Raise ε}) ∪ Eff(e₂)
``` ```
### M0 Exit Criteria ### M0 Exit Criteria (all CI-enforced)
1. All spec examples parse and pretty-print round-trip 1. Grammar compiles with zero ANTLR errors and zero warnings (`-Werror`)
2. No shift/reduce conflicts in grammar 2. All ten example programs parse (`./gradlew parseExamples`)
3. 10,000 random token sequences don't crash parser 3. Every ```mpl code block in the documentation parses (`DocumentationTest`)
4. Full test suite passes (`./gradlew test`)
Deferred to later milestones: pretty-print round-tripping and parser fuzzing.
## Implementation Roadmap ## Implementation Roadmap
1. **M0:** ANTLR grammar + 500 LOC test suite 1. **M0:** ANTLR grammar + 500 LOC test suite

24
precedence.csv
View file

@ -1,13 +1,15 @@
Level,Operators,Associativity,Description Level,Operators,Associativity,Description
9,function application,left,Function call f(x) or f x 11,"f(a, b) ‧ ⊕ ⊖ ↴{…}",left,"Postfix operators: function call, qualified module access, resource alloc/release, exception handler"
8,"↯ ✎ ? ⧈ ⏲ (prefix)",right,Unary prefix operators 10,"↯ ✎ ⧈ ⏲ - ⇀_ch ↽_ch (prefix)",right,"Unary prefix operators (including unary minus) and channel operations"
7,∘,left,Function composition 9,∘,left,Function composition
6,× ÷ ∗,left,Multiplication and division 8,× ÷ ∗,left,Multiplication and division (/ is an ASCII alias of ÷)
5,+ -,left,Addition and subtraction 7,+ -,left,Addition and subtraction
4,= ≠ < > ≤ ≥ ≈ ∼,non-associative,Comparison operators 6,= ≠ < > ≤ ≥ ≈ ∼,non-associative,Comparison operators
3,∧,left,Logical AND 5,∧,left,Logical AND
2,∨,left,Logical OR 4,∨,left,Logical OR
1,⟹,right,Implication 3,⟹,right,Implication / guard arrow
0,←,right,Assignment 2,|,left,Guarded alternatives: (condition ⟹ result) | fallback
1,←,right,Assignment
0,≜,right,Definition
-1,‖,left,Parallel composition -1,‖,left,Parallel composition
-2,;,left,Statement sequencing -2,;,left,Expression sequencing (trailing ; permitted)

1 Level Operators Associativity Description
2 9 11 function application f(a, b) ‧ ⊕ ⊖ ↴{…} left Function call f(x) or f x Postfix operators: function call, qualified module access, resource alloc/release, exception handler
3 8 10 ↯ ✎ ? ⧈ ⏲ (prefix) ↯ ✎ ⧈ ⏲ - ⇀_ch ↽_ch (prefix) right Unary prefix operators Unary prefix operators (including unary minus) and channel operations
4 7 9 ∘ left Function composition
5 6 8 × ÷ ∗ left Multiplication and division Multiplication and division (/ is an ASCII alias of ÷)
6 5 7 + - left Addition and subtraction
7 4 6 = ≠ < > ≤ ≥ ≈ ∼ non-associative Comparison operators
8 3 5 ∧ left Logical AND
9 2 4 ∨ left Logical OR
10 1 3 ⟹ right Implication Implication / guard arrow
11 0 2 ← | right left Assignment Guarded alternatives: (condition ⟹ result) | fallback
12 1 ← right Assignment
13 0 ≜ right Definition
14 -1 ‖ left Parallel composition
15 -2 ; left Statement sequencing Expression sequencing (trailing ; permitted)

10
road_map.md
View file

@ -19,7 +19,7 @@ The ANTLR grammar (`MPL.g4`) successfully defines 70+ mathematical symbols and c
- **Gap**: 100% of type system missing - **Gap**: 100% of type system missing
3. **Effect System Illusion** 3. **Effect System Illusion**
- Examples: `↴ {↯e ⇒ handler}` implies exception handling - Examples: `↴ {↯e ⟹ handler}` implies exception handling
- Grammar: Just parses symbols as operators - Grammar: Just parses symbols as operators
- Examples: `〔〕` claims automatic resource cleanup - Examples: `〔〕` claims automatic resource cleanup
- **Gap**: 100% of effect semantics missing - **Gap**: 100% of effect semantics missing
@ -177,8 +177,12 @@ public class SymbolicError {
**Goal**: Rich set of mathematical functions without English names **Goal**: Rich set of mathematical functions without English names
**Code Changes**: **Code Changes**:
```mpl These signatures are a design sketch for a future milestone — the symbols
-- Instead of "sort", "map", "filter": (→, ↑, ∃?, 📖, ✍, ⊤) are not in the M0 grammar, so the block is fenced as
plain text:
```text
-- Instead of "sort", "map", "filter": (design sketch, not yet parseable)
↑: List α → List α -- ascending order (up arrow) ↑: List α → List α -- ascending order (up arrow)
∀→: (α → β) → List α → List β -- universal transformation ∀→: (α → β) → List α → List β -- universal transformation
∃?: (α → 𝔹) → List α → List α -- exists predicate filter ∃?: (α → 𝔹) → List α → List α -- exists predicate filter

2
src/main/antlr4/MPL.g4
View file

@ -366,7 +366,7 @@ COLON : ':' ;
COMMA : ',' ; COMMA : ',' ;
UNDERSCORE : '_' ; UNDERSCORE : '_' ;
BAR : '|' ; BAR : '|' ;
MIDDOT : '‧' ; MIDDOT : '‧' | '\\middot' ;
// Identifiers. A leading underscore is NOT allowed: subscripts such as // Identifiers. A leading underscore is NOT allowed: subscripts such as
// ⌉_db_lock and ↽_socket must lex as UNDERSCORE + IDENTIFIER, not as a // ⌉_db_lock and ↽_socket must lex as UNDERSCORE + IDENTIFIER, not as a

11
src/test/java/com/mpl/test/DocumentationTest.java
View file

@ -24,6 +24,17 @@ public class DocumentationTest extends MPLTestBase {
assertAllMplBlocksParse(Paths.get("README.md")); assertAllMplBlocksParse(Paths.get("README.md"));
} }
@Test
public void testSpecCodeBlocksParse() throws IOException {
assertAllMplBlocksParse(Paths.get("math_prog_lang.md"));
}
@Test
public void testWhitepaperCodeBlocksParse() throws IOException {
assertAllMplBlocksParse(Paths.get("whitepaper", "mpl-whitepaper.md"));
assertAllMplBlocksParse(Paths.get("whitepaper", "mpl-whitepaper-appendices.md"));
}
private void assertAllMplBlocksParse(Path doc) throws IOException { private void assertAllMplBlocksParse(Path doc) throws IOException {
String content = Files.readString(doc); String content = Files.readString(doc);
Matcher m = MPL_BLOCK.matcher(content); Matcher m = MPL_BLOCK.matcher(content);

1
src/test/java/com/mpl/test/LexerTest.java
View file

@ -89,6 +89,7 @@ public class LexerTest extends MPLTestBase {
public void testModuleAccess() throws IOException { public void testModuleAccess() throws IOException {
assertTokenTypes("Mathematics‧sin", assertTokenTypes("Mathematics‧sin",
MPLLexer.IDENTIFIER, MPLLexer.MIDDOT, MPLLexer.IDENTIFIER); MPLLexer.IDENTIFIER, MPLLexer.MIDDOT, MPLLexer.IDENTIFIER);
assertTokenTypes("\\middot", MPLLexer.MIDDOT);
} }
@Test @Test

29
whitepaper/README.md
View file

@ -10,12 +10,12 @@ This directory contains the comprehensive academic whitepaper for the Mathematic
- Complete academic whitepaper in Markdown format - Complete academic whitepaper in Markdown format
- Suitable for online viewing and conversion to other formats - Suitable for online viewing and conversion to other formats
- Includes all sections from Abstract through Conclusion - Includes all sections from Abstract through Conclusion
- Features real-world application examples in 5 domains: - Features application sketches in 5 domains:
- Scientific Computing (ODE solvers) - Scientific Computing
- Financial Systems (Black-Scholes, VaR) - Data Processing
- Machine Learning (transformers, gradient descent) - Web Services
- Distributed Systems (Raft consensus, KV stores) - Machine Learning
- Quantum Computing (Grover's algorithm, teleportation) - Systems Programming
2. **`mpl-whitepaper.tex`** 2. **`mpl-whitepaper.tex`**
- Conference-ready LaTeX version (IEEE format) - Conference-ready LaTeX version (IEEE format)
@ -25,12 +25,11 @@ This directory contains the comprehensive academic whitepaper for the Mathematic
3. **`mpl-whitepaper-appendices.md`** 3. **`mpl-whitepaper-appendices.md`**
- Comprehensive appendices with: - Comprehensive appendices with:
- Complete symbol reference (70+ symbols) - Symbol reference (pointing to the authoritative glyph-escapes.md)
- Annotated example programs (10 examples) - Annotated example programs
- Grammar validation details - Grammar validation details
- Performance measurements
- Implementation details - Implementation details
- Future extensions roadmap - Pedagogy and envisioned pilot materials
## Whitepaper Structure ## Whitepaper Structure
@ -42,17 +41,17 @@ This directory contains the comprehensive academic whitepaper for the Mathematic
6. **Implementation** - ANTLR grammar and parser details 6. **Implementation** - ANTLR grammar and parser details
7. **Evaluation** - Completeness, performance, accessibility 7. **Evaluation** - Completeness, performance, accessibility
8. **Case Studies** - Concurrency, resources, metaprogramming 8. **Case Studies** - Concurrency, resources, metaprogramming
9. **Real-World Applications** - Scientific, financial, ML, distributed, quantum 9. **Real-World Applications** - Scientific, data, web, ML, systems
10. **Limitations & Future Work** - Current gaps and research directions 10. **Limitations & Future Work** - Current gaps and research directions
11. **Conclusion** - Vision for universal programming 11. **Conclusion** - Vision for universal programming
## Key Features Documented ## Key Features Documented
- **70+ Mathematical Symbols**: Complete Unicode operators with ASCII escapes - **70+ Mathematical Symbols**: Unicode operators, each with exactly one ASCII escape
- **11 Effect Operators**: Novel symbols for exceptions, concurrency, resources - **Effect Operators**: Novel symbols for exceptions, concurrency, resources
- **24 Greek Variables**: Full Greek alphabet for identifiers - **24 Greek Variables**: Full Greek alphabet for identifiers
- **Zero Ambiguities**: Validated grammar with precedence rules - **CI-Validated Grammar**: Compiles with zero ANTLR errors and warnings; documented precedence
- **Paradigm Coverage**: Functional, imperative, concurrent, OO, metaprogramming - **Paradigm Coverage**: Functional, imperative, concurrent, metaprogramming
## Building the LaTeX Version ## Building the LaTeX Version

413
whitepaper/mpl-whitepaper-appendices.md
View file

@ -2,127 +2,26 @@
## Appendix A: Complete Symbol Reference ## Appendix A: Complete Symbol Reference
### A.1 Core Mathematical Operators The authoritative symbol table — every glyph, its single ASCII escape, and
its Unicode code point — is maintained in one place:
[`glyph-escapes.md`](../glyph-escapes.md). It matches the lexer rules in
[`MPL.g4`](../src/main/antlr4/MPL.g4) exactly. A duplicate table here would
drift; earlier versions of this appendix did exactly that.
#### Greek Letters (Variables) In summary, the M0 symbol set comprises:
All 24 Greek letters serve as single-character identifiers, following mathematical convention:
| Symbol | ASCII Escape | Unicode | Mathematical Usage | MPL Usage | - **24 Greek letters** (α…ω) as variables, with λ doubling as the lambda binder
|--------|-------------|---------|-------------------|-----------| - **Logic**: ∧ ∨ ⟹ ∀
| α | `\alpha` | U+03B1 | Angle, coefficient | General variable | - **Arithmetic**: + - × ÷ (ASCII alias `/`) ∗ ∘, with unary minus
| β | `\beta` | U+03B2 | Angle, coefficient | General variable | - **Comparisons**: = ≠ < > ≤ ≥ ≈ ∼
| γ | `\gamma` | U+03B3 | Euler constant | General variable | - **Sets and types**: ∅ ∈ ℕ ℤ ℚ ℝ ℂ 𝔹 ⊥
| δ | `\delta` | U+03B4 | Small change | General variable | - **Definition and assignment**: ≜ and ←
| ε | `\epsilon` | U+03B5 | Small positive | General variable | - **Output**: ✎ (the one output operator)
| ζ | `\zeta` | U+03B6 | Zeta function | General variable | - **Effects**: ↯ ↴ ‖ ⌈⌉ ⊕ ⊖ ⇀ ↽ ⏲ ⧈ ⟳ 〔〕
| η | `\eta` | U+03B7 | Efficiency | General variable | - **Modules and metaprogramming**: 𝓜 ⇒ ‧ 🖫 ⌜⌝ ⌞⌟ ⟨⟩
| θ | `\theta` | U+03B8 | Angle | General variable |
| ι | `\iota` | U+03B9 | Imaginary unit | General variable |
| κ | `\kappa` | U+03BA | Curvature | General variable |
| λ | `\lambda`, `\lam` | U+03BB | Eigenvalue | Lambda/function |
| μ | `\mu` | U+03BC | Mean, measure | General variable |
| ν | `\nu` | U+03BD | Frequency | General variable |
| ξ | `\xi` | U+03BE | Random variable | General variable |
| ο | `\omicron` | U+03BF | - | General variable |
| π | `\pi` | U+03C0 | Pi constant | Variable/constant |
| ρ | `\rho` | U+03C1 | Density | General variable |
| σ | `\sigma` | U+03C3 | Standard deviation | General variable |
| τ | `\tau` | U+03C4 | Time constant | General variable |
| υ | `\upsilon` | U+03C5 | - | General variable |
| φ | `\phi` | U+03C6 | Golden ratio | General variable |
| χ | `\chi` | U+03C7 | Chi distribution | General variable |
| ψ | `\psi` | U+03C8 | Wave function | General variable |
| ω | `\omega` | U+03C9 | Angular velocity | General variable |
#### Logical Operators Symbols reserved for M1 (∪ ∩ ⊂ ⊆ ∉ ¬ ⟺ ∃ → ⇐ ∑ √ ² % ? and friends) are
listed at the end of `glyph-escapes.md`; they are not in the grammar.
| Symbol | ASCII Escape | Unicode | Precedence | Associativity | Description |
|--------|-------------|---------|------------|---------------|-------------|
| ∧ | `\and`, `\wedge` | U+2227 | 3 | Left | Logical AND |
| ∨ | `\or`, `\vee` | U+2228 | 2 | Left | Logical OR |
| ¬ | `\not`, `\neg` | U+00AC | 8 | Prefix | Logical NOT |
| ⟹ | `\implies`, `\Rightarrow` | U+27F9 | 1 | Right | Implication |
| ⟺ | `\iff`, `\Leftrightarrow` | U+27FA | 1 | Right | If and only if |
| ∀ | `\forall` | U+2200 | - | - | Universal quantifier |
| ∃ | `\exists` | U+2203 | - | - | Existential quantifier |
#### Arithmetic Operators
| Symbol | ASCII Escape | Unicode | Precedence | Associativity | Description |
|--------|-------------|---------|------------|---------------|-------------|
| + | - | U+002B | 5 | Left | Addition |
| - | - | U+002D | 5 | Left | Subtraction |
| × | `\times` | U+00D7 | 6 | Left | Multiplication |
| ÷ | `\div` | U+00F7 | 6 | Left | Division |
| ^ | - | U+005E | 7 | Right | Exponentiation |
| √ | `\sqrt` | U+221A | 8 | Prefix | Square root |
| Σ | `\sum` | U+2211 | - | - | Summation |
#### Set Theory Operators
| Symbol | ASCII Escape | Unicode | Description |
|--------|-------------|---------|-------------|
| ∅ | `\emptyset` | U+2205 | Empty set |
| ∈ | `\in` | U+2208 | Element of |
| ∉ | `\notin` | U+2209 | Not element of |
| ⊂ | `\subset` | U+2282 | Proper subset |
| ⊆ | `\subseteq` | U+2286 | Subset or equal |
| ∪ | `\union`, `\cup` | U+222A | Set union |
| ∩ | `\intersect`, `\cap` | U+2229 | Set intersection |
| \| | - | U+007C | Set size/cardinality |
#### Comparison Operators
| Symbol | ASCII Escape | Unicode | Precedence | Description |
|--------|-------------|---------|------------|-------------|
| = | - | U+003D | 4 | Equality |
| ≠ | `\neq`, `\ne` | U+2260 | 4 | Not equal |
| < | - | U+003C | 4 | Less than |
| > | - | U+003E | 4 | Greater than |
| ≤ | `\leq`, `\le` | U+2264 | 4 | Less or equal |
| ≥ | `\geq`, `\ge` | U+2265 | 4 | Greater or equal |
| ≈ | `\approx` | U+2248 | 4 | Approximately |
### A.2 Programming Extensions
#### I/O and Assignment
| Symbol | ASCII Escape | Unicode | Usage | Example |
|--------|-------------|---------|-------|---------|
| ✎ | `\pencil` | U+270E | Output/print | `✎ "Hello"` |
| ← | `\leftarrow`, `\gets` | U+2190 | Assignment | `x ← 42` |
| → | `\rightarrow`, `\to` | U+2192 | Function type | `ℕ → ℕ` |
| ≜ | `\coloneq` | U+225C | Definition | `fact ≜ λn: ...` |
#### Exception Handling
| Symbol | ASCII Escape | Unicode | Usage | Example |
|--------|-------------|---------|-------|---------|
| ↯ | `\lightning` | U+21AF | Raise exception | `↯"Error!"` |
| ↴ | `\downarrow` | U+21B4 | Handle exception | `expr ↴ {handler}` |
#### Concurrency
| Symbol | ASCII Escape | Unicode | Usage | Example |
|--------|-------------|---------|-------|---------|
| ‖ | `\parallel` | U+2016 | Parallel composition | `task1 ‖ task2` |
| ⇀ | `\send` | U+21C0 | Channel send | `value ⇀ channel` |
| ↽ | `\receive` | U+21BD | Channel receive | `↽ channel` |
#### Resource Management
| Symbol | ASCII Escape | Unicode | Usage | Example |
|--------|-------------|---------|-------|---------|
| ⊕ | `\oplus` | U+2295 | Resource acquire | `file ← ⊕open(path)` |
| ⊖ | `\ominus` | U+2296 | Resource release | `⊖file` |
| 〔〕 | `\lbracket`, `\rbracket` | U+3014/5 | RAII scope | `〔resource ops〕` |
#### Type Symbols
| Symbol | ASCII Escape | Unicode | Type | Set Definition |
|--------|-------------|---------|------|----------------|
| ℕ | `\nat`, `\N` | U+2115 | Natural numbers | {0, 1, 2, ...} |
| ℤ | `\int`, `\Z` | U+2124 | Integers | {..., -2, -1, 0, 1, 2, ...} |
| ℚ | `\rat`, `\Q` | U+211A | Rational numbers | {p/q : p,q ∈ ℤ, q ≠ 0} |
| ℝ | `\real`, `\R` | U+211D | Real numbers | Complete ordered field |
| ℂ | `\complex`, `\C` | U+2102 | Complex numbers | {a + bi : a,b ∈ ℝ} |
| 𝔹 | `\bool`, `\B` | U+1D539 | Booleans | {true, false} |
## Appendix B: Annotated Example Programs ## Appendix B: Annotated Example Programs
@ -141,10 +40,10 @@ All 24 Greek letters serve as single-character identifiers, following mathematic
#### Month 3: Variables and Arithmetic #### Month 3: Variables and Arithmetic
```mpl ```mpl
-- Calculate rectangle area -- Calculate rectangle area
ℓ ← 5 -- length L ← 5; -- length
w ← 3 -- width w ← 3; -- width
A ← ℓ × w -- area formula A ← L × w; -- area formula
✎ A -- output: 15 ✎ A -- prints 15 (once MPL executes)
``` ```
**Annotations:** **Annotations:**
- `←` (left arrow): Assignment matches math notation - `←` (left arrow): Assignment matches math notation
@ -155,9 +54,10 @@ A ← ℓ × w -- area formula
#### Month 6: Loops and Summation #### Month 6: Loops and Summation
```mpl ```mpl
-- Sum numbers 1 to 10 -- Sum numbers 1 to 10
Σ ← 0 numbers ← [1, 2, 3, 4, 5, 6, 7, 8, 9, 10];
∀ n ∈ [1..10]: Σ ← Σ + n total ← 0;
✎ "Sum: " + Σ ∀ n ∈ numbers : total ← total + n;
✎("Sum: " + total)
``` ```
**Annotations:** **Annotations:**
- `∀` (for all): Universal quantifier for iteration - `∀` (for all): Universal quantifier for iteration
@ -168,10 +68,10 @@ A ← ℓ × w -- area formula
#### Month 6: Conditional Logic #### Month 6: Conditional Logic
```mpl ```mpl
-- Classify a number -- Classify a number
x ← -5 x ← -5;
x < 0 ⟹ ✎ "Negative" (x < 0 ⟹ ✎"Negative") |
x = 0 ⟹ ✎ "Zero" (x = 0 ⟹ ✎"Zero") |
x > 0 ⟹ ✎ "Positive" (x > 0 ⟹ ✎"Positive")
``` ```
**Annotations:** **Annotations:**
- `⟹` (implies): If-then as logical implication - `⟹` (implies): If-then as logical implication
@ -181,9 +81,9 @@ x > 0 ⟹ ✎ "Positive"
#### Month 6: Recursion (Factorial) #### Month 6: Recursion (Factorial)
```mpl ```mpl
-- Factorial function -- Factorial function
fact ≜ λn: n ≤ 1 ⟹ 1 ∣ n × fact(n - 1) fact ≜ λn: (n ≤ 1 ⟹ 1) | (n × fact(n - 1));
✎ fact(5) -- Output: 120 ✎ fact(5) -- 120 (once MPL executes)
``` ```
**Annotations:** **Annotations:**
- `≜` (define as): Function definition - `≜` (define as): Function definition
@ -194,42 +94,38 @@ fact ≜ λn: n ≤ 1 ⟹ 1 ∣ n × fact(n - 1)
### B.2 Advanced Examples ### B.2 Advanced Examples
#### Quadratic Solver #### Quadratic Solver
```mpl The quadratic solver below is an M1+ design sketch — it uses ², √ and
-- Solve ax² + bx + c = 0 subscripts, which are not yet in the grammar, so it is fenced as plain text:
```text
-- Solve ax² + bx + c = 0 (M1+ design sketch, not yet parseable)
quadratic ≜ λa,b,c: quadratic ≜ λa,b,c:
Δ ← b² - 4×a×c Δ ← b² - 4×a×c;
Δ < 0 ⟹ ✎ "No real solutions" (Δ < 0 ⟹ ✎"No real solutions") |
Δ = 0 ⟹ ✎ "One solution: " + (-b÷(2×a)) (Δ = 0 ⟹ ✎("One solution: " + (-b÷(2×a)))) |
Δ > 0 ⟹ (Δ > 0 ⟹ ✎("Two solutions: " + ((-b + √Δ) ÷ (2×a)) + ", " + ((-b - √Δ) ÷ (2×a))))
r₁ ← (-b + √Δ) ÷ (2×a)
r₂ ← (-b - √Δ) ÷ (2×a)
✎ "Two solutions: " + r₁ + ", " + r₂
``` ```
#### List Processing #### List Processing
```mpl Set comprehensions and `mod` are M1+ design sketches, so this block is
-- Filter and map fenced as plain text:
numbers ← [1, 2, 3, 4, 5, 6, 7, 8, 9, 10]
-- Get even numbers ```text
evens ← {n ∈ numbers | n mod 2 = 0} -- Filter and map (M1+ design sketch, not yet parseable)
numbers ← [1, 2, 3, 4, 5, 6, 7, 8, 9, 10];
-- Square them evens ← {n ∈ numbers | n mod 2 = 0};
squares ← {n² | n ∈ evens} squares ← {n² | n ∈ evens};
✎ squares
✎ squares -- Output: [4, 16, 36, 64, 100]
``` ```
#### Error Handling #### Error Handling
```mpl ```mpl
-- Safe division with exceptions -- Safe division with exceptions
safeDivide ≜ λx,y: safeDivide ≜ λx, y: (y = 0 ⟹ ↯"Division by zero!") | (x ÷ y);
y = 0 ⟹ ↯"Division by zero!"
x ÷ y
-- Using with handler -- Using with handler
result ← safeDivide(10, 0) ↴ { result ← safeDivide(10, 0) ↴ {
↯"Division by zero!" ⟹ ✎ "Error caught" ↯"Division by zero!" ⟹ ✎"Error caught";
↯e ⟹ ↯e -- Re-raise other errors ↯e ⟹ ↯e -- Re-raise other errors
} }
``` ```
@ -237,139 +133,132 @@ result ← safeDivide(10, 0) ↴ {
#### Concurrent Downloads #### Concurrent Downloads
```mpl ```mpl
-- Download multiple URLs in parallel -- Download multiple URLs in parallel
urls ← ["http://a.com", "http://b.com", "http://c.com"] urls ← ["http://a.com", "http://b.com", "http://c.com"];
-- Launch parallel downloads -- Launch parallel downloads, sending each result to the results channel
∀ url ∈ urls: ∀ url ∈ urls : ⇀_results fetch(url);
fetch(url) ⇀ results ‖
-- Collect results -- Collect results
∀ i ∈ [1..|urls|]: ∀ url ∈ urls : (
data ← ↽results data ← ↽_results url;
✎ "Downloaded: " + |data| + " bytes" ✎("Downloaded: " + size(data) + " bytes")
)
``` ```
#### File Processing with RAII #### File Processing with RAII
```mpl ```mpl
-- Process file with automatic cleanup -- Process file with automatic cleanup
processFile ≜ λpath: 〔 processFile ≜ λpath: 〔
file ← ⊕open(path) -- Acquire file ← open(path) ⊕; -- Acquire
lines ← readLines(file) lines ← readLines(file);
∀ line ∈ lines: ∀ line ∈ lines : (
words ← split(line, " ") words ← split(line, " ");
✎ "Word count: " + |words| ✎("Word count: " + count(words))
)
-- file automatically released here {- file automatically released here -}
〕 〕;
``` ```
### B.3 Real-World Application Examples ### B.3 Real-World Application Examples
#### Data Analysis #### Data Analysis
```mpl ∑, √ and ² are M1, so the statistics sketch is fenced as plain text:
-- Statistical analysis
analyze ≜ λdata:
n ← |data|
μ ← (Σ x ∈ data: x) ÷ n -- mean
σ² ← (Σ x ∈ data: (x-μ)²) ÷ n -- variance
σ ← √σ² -- std dev
✎ "n=" + n + ", μ=" + μ + ", σ=" + σ ```text
-- Statistical analysis (M1+ design sketch, not yet parseable)
analyze ≜ λdata:
n ← |data|;
μ ← (∑ x ∈ data: x) ÷ n;
σ² ← (∑ x ∈ data: (x-μ)²) ÷ n;
σ ← √σ²;
✎("n=" + n + ", μ=" + μ + ", σ=" + σ)
``` ```
#### Simple Web Server #### Simple Web Server
```mpl Record field access (`req.path`) is M1, so the HTTP-server sketch is
-- HTTP server fenced as plain text:
server ≜ λport:
∀ req ∈ listen(port): ```text
-- Handle request in parallel -- HTTP server (M1+ design sketch, not yet parseable)
handleRequest(req) ‖ server ≜ λport: ∀ req ∈ listen(port): handleRequest(req) ‖ acceptNext();
handleRequest ≜ λreq: handleRequest ≜ λreq:
req.path = "/" ⟹ (req.path = "/" ⟹ respond(200, "<h1>Welcome!</h1>")) |
respond(200, "<h1>Welcome!</h1>") (req.path = "/api/data" ⟹ respond(200, getData())) |
req.path = "/api/data" ⟹
respond(200, getData())
true ⟹ -- default case
respond(404, "Not found") respond(404, "Not found")
``` ```
#### Machine Learning - Perceptron #### Machine Learning - Perceptron
```mpl ∑, indexing and field access are M1, so the perceptron sketch is fenced
-- Simple perceptron as plain text:
```text
-- Simple perceptron (M1+ design sketch, not yet parseable)
perceptron ≜ λweights, bias: perceptron ≜ λweights, bias:
λinputs: λinputs:
z ← (Σ i ∈ [1..|inputs|]: z ← (∑ i ∈ [1..|inputs|]: weights[i] × inputs[i]) + bias;
weights[i] × inputs[i]) + bias (z > 0 ⟹ 1) | 0 -- Step activation
z > 0 ⟹ 1 ∣ 0 -- Step activation
-- Training step
train ≜ λp, inputs, target, α: train ≜ λp, inputs, target, α:
output ← p(inputs) output ← p(inputs);
error ← target - output error ← target - output;
∀ i ∈ [1..|inputs|]: p.weights[i] ← p.weights[i] + α×error×inputs[i];
-- Update weights
∀ i ∈ [1..|inputs|]:
p.weights[i] ← p.weights[i] + α×error×inputs[i]
p.bias ← p.bias + α×error p.bias ← p.bias + α×error
``` ```
## Appendix C: Grammar Validation ## Appendix C: Grammar Validation
### C.1 ANTLR 4 Grammar Statistics ### C.1 ANTLR 4 Grammar Validation
**Grammar Metrics:** The authoritative grammar is [`MPL.g4`](../src/main/antlr4/MPL.g4). Instead
- Total Lines: 373 of quoting statistics that drift, CI enforces these properties on every push:
- Parser Rules: 32
- Lexer Rules: 89
- Unique Operators: 71
- Precedence Levels: 12
- Unicode Code Points: 76
**Validation Results:** - The grammar compiles under ANTLR 4.13 with **warnings treated as errors**
``` (`-Werror`), so left recursion, token shadowing and unreachable
ANTLR 4.9.3 Grammar Analysis alternatives fail the build
============================ - All ten example programs parse (`./gradlew parseExamples`)
Grammar: MPL.g4 - Every ```mpl code block in the documentation parses (`DocumentationTest`)
Conflicts: 0 - Start symbol: `program`; target: Java
Ambiguities: 0
Left Recursion: Resolved
Start Symbol: program
Target: Java
```
### C.2 Precedence Table ### C.2 Precedence Table
Full precedence hierarchy with examples: Authoritative copy: [`precedence.csv`](../precedence.csv).
| Level | Operators | Example | Parses As | | Level | Operators | Example | Parses As |
|-------|-----------|---------|-----------| |-------|-----------|---------|-----------|
| -2 | `;` | `a; b; c` | `((a); b); c` | | 11 | `f(a,b)` `‧` `⊕` `⊖` `↴{…}` | `M‧f(x)⊕` | `((M‧f)(x))⊕` |
| 10 | `↯ ✎ ⧈ ⏲ -` (prefix), `⇀_ch ↽_ch` | `✎ -a` | `✎(-a)` |
| 9 | `∘` | `f ∘ g ∘ h` | `(f ∘ g) ∘ h` |
| 8 | `×,÷,∗` | `a × b ÷ c` | `(a × b) ÷ c` |
| 7 | `+,-` | `a + b - c` | `(a + b) - c` |
| 6 | `=,≠,<,>,≤,≥,≈,∼` | `a < b = c` | Error (non-assoc) |
| 5 | `∧` | `a ∧ b ∧ c` | `(a ∧ b) ∧ c` |
| 4 | `∨` | `a ∨ b ∨ c` | `(a ∨ b) ∨ c` |
| 3 | `⟹` | `a ⟹ b ⟹ c` | `a ⟹ (b ⟹ c)` |
| 2 | `\|` | `a ⟹ b \| c` | `(a ⟹ b) \| c` |
| 1 | `←` | `a ← b ← c` | `a ← (b ← c)` |
| 0 | `≜` | `f ≜ g ≜ h` | `f ≜ (g ≜ h)` |
| -1 | `‖` | `a ‖ b ‖ c` | `(a ‖ b) ‖ c` | | -1 | `‖` | `a ‖ b ‖ c` | `(a ‖ b) ‖ c` |
| 0 | `←` | `a ← b ← c` | `a ← (b ← c)` | | -2 | `;` | `a; b; c` | `(a; b); c` |
| 1 | `⟹` | `a ⟹ b ⟹ c` | `a ⟹ (b ⟹ c)` |
| 2 | `∨` | `a ∨ b ∨ c` | `(a ∨ b) ∨ c` |
| 3 | `∧` | `a ∧ b ∧ c` | `(a ∧ b) ∧ c` |
| 4 | `=,<,>` | `a < b = c` | Error (non-assoc) |
| 5 | `+,-` | `a + b - c` | `(a + b) - c` |
| 6 | `×,÷` | `a × b ÷ c` | `(a × b) ÷ c` |
| 7 | `^` | `a ^ b ^ c` | `a ^ (b ^ c)` |
| 8 | `√,¬,↯` | `√√a` | `√(√a)` |
| 9 | _(app)_ | `f g h` | `(f g) h` |
### C.3 Ambiguity Resolution Examples ### C.3 Disambiguation Rules
**Lambda vs Variable λ** **Lambda vs Variable λ**
- Context: `λ` as operator vs Greek variable - Context: `λ` opens a lambda and is also a Greek variable
- Resolution: Grammar rule precedence - Resolution: one token (`LAMBDA_VAR`); the parser decides by position
- Test: `λ ← λx: x` parses correctly - Test: `λ ← λx: x;` parses (assign a lambda to the variable λ)
**Application vs Multiplication** **Braces: record vs set vs block**
- Context: `f g` (application) vs `a × b` - `{a: e, …}` is a record, `{a, b, …}` (two or more elements) is a set,
- Resolution: Whitespace-sensitive lexing everything else — including `{}` and `{x}` — is a block
- Test: `f g×h` parses as `App(f, Mul(g, h))` - A singleton set literal cannot be written in M0 (documented in
DECISIONS.md)
**The bar `|`**
- One BAR token serves guarded alternatives; the `|` inside `⟨a|b⟩` is the
guarded-alternative level of the inner expression
## Appendix D: Symbol Pedagogy Guide ## Appendix D: Symbol Pedagogy Guide
@ -388,7 +277,7 @@ Full precedence hierarchy with examples:
**Progressive Introduction**: **Progressive Introduction**:
1. Start with simple: `λx: x + 1` 1. Start with simple: `λx: x + 1`
2. Multiple parameters: `λx,y: x + y` 2. Multiple parameters: `λx,y: x + y`
3. With conditions: `λn: n > 0 ⟹ n ∣ 0` 3. With conditions: `λn: (n > 0 ⟹ n) | 0`
#### Teaching ∀ (For All/Loops) #### Teaching ∀ (For All/Loops)
**Physical Activity**: "Everyone Does" **Physical Activity**: "Everyone Does"
@ -400,9 +289,9 @@ Full precedence hierarchy with examples:
- ∀ x ∈ {1,2,3}: means "do for 1, then 2, then 3" - ∀ x ∈ {1,2,3}: means "do for 1, then 2, then 3"
**Code Progression**: **Code Progression**:
1. Simple iteration: `∀ n ∈ [1..5]: ✎ n` 1. Simple iteration: `∀ n ∈ [1, 2, 3, 4, 5] : ✎ n`
2. With accumulation: `∀ n ∈ list: sum ← sum + n` 2. With accumulation: `∀ n ∈ list: sum ← sum + n`
3. Nested loops: `∀ i ∈ [1..3]: ∀ j ∈ [1..3]: ✎(i,j)` 3. Nested loops: `∀ i ∈ [1, 2, 3] : ∀ j ∈ [1, 2, 3] : ✎(i + j)`
#### Teaching ✎ (Output) #### Teaching ✎ (Output)
**Physical Activity**: "Pencil and Paper" **Physical Activity**: "Pencil and Paper"
@ -427,13 +316,13 @@ Full precedence hierarchy with examples:
**Week 3: Control Flow** **Week 3: Control Flow**
- ⟹ (if-then) - ⟹ (if-then)
- ∣ (else) - | (fallback: `(condition ⟹ result) | fallback`)
- Simple conditions - Simple conditions
**Week 4: Loops** **Week 4: Loops**
- ∀ (for all) - ∀ (for all)
- ∈ (element of) - ∈ (element of)
- Ranges: [1..10] - List literals: [1, 2, 3]
**Week 5: Functions** **Week 5: Functions**
- λ (lambda) - λ (lambda)
@ -447,12 +336,13 @@ Full precedence hierarchy with examples:
## Appendix E: Implementation Details ## Appendix E: Implementation Details
### E.1 Unicode Normalization ### E.1 Unicode Normalization (planned)
All input undergoes Unicode normalization to NFC: Input should undergo Unicode normalization to NFC before lexing. This is
planned; the current parser consumes code points as-is:
```java ```java
// Ensure consistent handling // Planned: ensure consistent handling
String normalize(String input) { String normalize(String input) {
return Normalizer.normalize(input, Normalizer.Form.NFC); return Normalizer.normalize(input, Normalizer.Form.NFC);
} }
@ -464,22 +354,28 @@ Context-aware error reporting maintains symbol clarity:
``` ```
Error at line 3:14: Expected '⟹' after condition Error at line 3:14: Expected '⟹' after condition
x < 0 ∣ "negative" x < 0 | "negative"
^ ^
Hint: Use '⟹' for if-then. '∣' is only for else-branches. Hint: A guard needs an arrow: (x < 0 ⟹ "negative") | fallback.
``` ```
(Illustrative; today the parser emits standard ANTLR diagnostics.)
### E.3 ASCII Escape Processing ### E.3 ASCII Escape Processing
Flexible escape sequences with shortcuts: Each glyph has exactly one ASCII escape, defined as a lexer alternative
(the full table is [`glyph-escapes.md`](../glyph-escapes.md)):
```antlr ```antlr
LAMBDA : 'λ' | '\\lambda' | '\\lam' ; LAMBDA_VAR : 'λ' | '\\lambda' ;
FORALL : '∀' | '\\forall' | '\\all' ; FORALL : '∀' | '\\forall' ;
IMPLIES : '⟹' | '\\implies' | '\\=>' ; IMPLIES : '⟹' | '\\implies' ;
``` ```
## Appendix F: Input Method Documentation ## Appendix F: Input Method Documentation (envisioned)
Only the ASCII escapes exist today; everything else in this appendix is
tooling we want to build.
### F.1 Visual Palette ### F.1 Visual Palette
@ -491,10 +387,11 @@ IMPLIES : '⟹' | '\\implies' | '\\=>' ;
### F.2 Text Shortcuts ### F.2 Text Shortcuts
**Common Patterns**: The lexer accepts exactly one escape per glyph (`\lambda`, `\forall`, …).
- `\lam` → λ (shorter than `\lambda`) Editor-side auto-replace could additionally offer shorthand that expands to
- `\all` → ∀ (shorter than `\forall`) the glyph before the code ever reaches the lexer:
- `->` → → (arrow shortcuts)
- `\lam` → λ (editor expands; the lexer itself only accepts `\lambda`)
- `:=` → ≜ (definition) - `:=` → ≜ (definition)
- `!=` → ≠ (not equal) - `!=` → ≠ (not equal)

113
whitepaper/mpl-whitepaper.md
View file

@ -6,7 +6,7 @@
## Abstract ## Abstract
In a school in Cairo, a 10-year-old girl named Fatima watches her teacher write a simple computer program on the board. The code is full of foreign words that might as well be magic spells to her Arabic-speaking mind. This scene repeats in classrooms worldwide, where virtually all mainstream programming languages impose English keywords as fundamental syntax, creating cognitive friction for the 80% of humanity who don't speak English. This paper presents Mathematical Programming Language (MPL), a novel approach that replaces traditional keywords with mathematical notation—humanity's existing universal language. MPL demonstrates that a complete, production-ready programming language can be built entirely from mathematical symbols while maintaining full expressiveness across all programming paradigms. Our implementation consists of an ANTLR 4 grammar supporting over 70 Unicode mathematical operators, 24 Greek letter variables, and novel effect operators for computational effects. Through hypothetical scenarios like a student's journey from printing "Jambo!" to teaching peers within one year, we envision potential improvements in learning metrics: First Program Time could be reduced from days to minutes, retention rates might exceed traditional approaches, and teachers could enthusiastically adopt MPL in non-English classrooms. MPL proves that cognitive universality in programming languages is not just theoretically possible but practically achievable, opening a path toward truly global programming tools that transcend linguistic boundaries and enable cognitive justice in technology education. In a school in Cairo, a 10-year-old girl named Fatima watches her teacher write a simple computer program on the board. The code is full of foreign words that might as well be magic spells to her Arabic-speaking mind. This scene repeats in classrooms worldwide, where virtually all mainstream programming languages impose English keywords as fundamental syntax, creating cognitive friction for the 80% of humanity who don't speak English. This paper presents Mathematical Programming Language (MPL), a novel approach that replaces traditional keywords with mathematical notation—humanity's existing universal language. MPL demonstrates that a programming language can be built entirely from mathematical symbols; the current milestone is a fully working parser, with execution to follow. Our implementation consists of an ANTLR 4 grammar supporting over 70 Unicode mathematical operators, 24 Greek letter variables, and novel effect operators for computational effects. Through hypothetical scenarios like a student's journey from printing "Jambo!" to teaching peers within one year, we envision potential improvements in learning metrics: First Program Time could be reduced from days to minutes, retention rates might exceed traditional approaches, and teachers could enthusiastically adopt MPL in non-English classrooms. MPL proves that cognitive universality in programming languages is not just theoretically possible but practically achievable, opening a path toward truly global programming tools that transcend linguistic boundaries and enable cognitive justice in technology education.
## I. Introduction ## I. Introduction
@ -98,7 +98,7 @@ MPL builds on established mathematical notation:
- **Logical Operators**: ∧ (and), ∨ (or), ¬ (not), ⟹ (implies) - **Logical Operators**: ∧ (and), ∨ (or), ¬ (not), ⟹ (implies)
- **Quantifiers**: ∀ (forall), ∃ (exists), λ (lambda) - **Quantifiers**: ∀ (forall), ∃ (exists), λ (lambda)
- **Relations**: =, ≠, <, ≤, ≈ - **Relations**: =, ≠, <, ≤, ≈
- **Arithmetic**: +, -, ×, ÷, ^, √ - **Arithmetic**: +, -, ×, ÷ (^ and √ arrive with defined semantics in M1)
- **Types**: ℕ (natural), ℤ (integer), ℝ (real), 𝔹 (boolean) - **Types**: ℕ (natural), ℤ (integer), ℝ (real), 𝔹 (boolean)
### B. Programming Extensions ### B. Programming Extensions
@ -111,7 +111,7 @@ MPL introduces intuitive symbols for computational concepts:
- **Concurrency**: ‖ (parallel bars) for parallel execution - **Concurrency**: ‖ (parallel bars) for parallel execution
- **Resources**: ⊕/⊖ (circled plus/minus) for acquire/release - **Resources**: ⊕/⊖ (circled plus/minus) for acquire/release
These symbols were chosen through extensive testing with educators and children, ensuring each passes the Fatima Test. These symbols were chosen to pass the Fatima Test; empirical validation with educators and children is planned, not yet performed.
### C. Real Code Examples ### C. Real Code Examples
@ -124,9 +124,9 @@ Here's "Hello World" in MPL – as simple as a hypothetical student's first prog
A more complex example calculating rectangle area: A more complex example calculating rectangle area:
```mpl ```mpl
ℓ ← 5 L ← 5;
w ← 3 w ← 3;
A ← ℓ × w A ← L × w;
✎ A ✎ A
``` ```
@ -136,27 +136,31 @@ A ← ℓ × w
The MPL implementation consists of: The MPL implementation consists of:
- **ANTLR 4 Grammar**: 373 lines defining complete syntax - **ANTLR 4 Grammar**: the complete M0 syntax, compiled with warnings treated as errors
- **Unicode Normalization**: Ensures é and é are treated identically - **ASCII Fallbacks**: every symbol has exactly one text escape (λ → `\lambda`)
- **ASCII Fallbacks**: Every symbol has text escapes (λ → `\lambda`) - **Multi-platform Support**: runs on any Unicode-capable system
- **Multi-platform Support**: Runs on any Unicode-capable system - **Unicode Normalization**: planned (the parser currently consumes code points as-is)
### B. Parser Validation ### B. Parser Validation
- Zero ambiguities across all test programs Everything in this list is enforced by CI on every push:
- 12-level precedence hierarchy matching mathematical conventions
- Round-trip testing between Unicode and ASCII forms
- Tested on example programs
### C. Educational Tools - The grammar compiles with zero ANTLR errors and zero warnings
- All ten example programs parse
- Every ```mpl code block in the project documentation parses
- The precedence chain is documented in `precedence.csv` and exercised by the test suite
Beyond the core language, we've developed: ### C. Educational Tools (envisioned)
Beyond the core language, we envision:
- Visual symbol palettes for beginners - Visual symbol palettes for beginners
- Voice input for multiple languages - Voice input for multiple languages
- Handwriting recognition for natural input - Handwriting recognition for natural input
- Integration with standard editors - Integration with standard editors
None of these exist yet; today the ASCII escapes are the portable input method.
## VI. Evaluation ## VI. Evaluation
### A. Hypothetical Learning Journey ### A. Hypothetical Learning Journey
@ -171,16 +175,16 @@ Hypothesis: First Program Time could be minutes rather than days.
**Building on math knowledge**: They could apply familiar mathematical concepts: **Building on math knowledge**: They could apply familiar mathematical concepts:
```mpl ```mpl
ℓ ← 5 L ← 5;
w ← 3 w ← 3;
A ← ℓ × w A ← L × w;
✎ A ✎ A
``` ```
**Advanced concepts**: Mathematical notation could make loops intuitive: **Advanced concepts**: Mathematical notation could make loops intuitive:
```mpl ```mpl
Σ ← 0 total ← 0;
∀ n ∈ [1..10]: Σ ← Σ + n ∀ n ∈ [1, 2, 3, 4, 5] : total ← total + n
``` ```
**Potential outcome**: Students might progress from beginners to teaching others within a year. **Potential outcome**: Students might progress from beginners to teaching others within a year.
@ -201,10 +205,9 @@ We hypothesize that MPL could improve three key metrics:
While human outcomes are primary, technical validation shows: While human outcomes are primary, technical validation shows:
- Complete coverage of programming paradigms - The ten example programs cover functional, concurrent, resource-managed, metaprogramming and module-based code, and all parse in CI
- 70+ operators handling all computational needs - Every symbol has exactly one meaning and one ASCII escape
- Successful parsing of complex real-world programs - The M0 grammar compiles with zero ANTLR errors and warnings
- No loss of expressiveness compared to English-based languages
### D. Current Implementation Limitations ### D. Current Implementation Limitations
@ -239,59 +242,59 @@ We hypothesize that pilot programs could reveal:
## VIII. Real-World Applications ## VIII. Real-World Applications
MPL's mathematical syntax proves powerful across domains: MPL's mathematical syntax proves powerful across domains. Every block below
parses with the shipped M0 grammar (this is CI-checked); where richer
notation (∑, √, ², subscripts, tuples) is planned for M1, the examples use
plain M0 syntax instead.
### A. Scientific Computing ### A. Scientific Computing
```mpl ```mpl
-- Runge-Kutta ODE solver -- Fixed-step numerical integration (Euler method)
rk4 ≜ λf,y₀,t₀,t₁,h: euler ≜ λf, y, t, h, steps: ∀step∈countTo(steps): (
steps ← ⌊(t₁ - t₀) ÷ h⌋ y ← y + h × f(t, y);
evolve ← λ(t,y): t ← t + h
k₁ ← h × f(t, y) );
k₂ ← h × f(t + h÷2, y + k₁÷2)
k₃ ← h × f(t + h÷2, y + k₂÷2)
k₄ ← h × f(t + h, y + k₃)
(t + h, y + (k₁ + 2×k₂ + 2×k₃ + k₄)÷6)
iterate(evolve, (t₀,y₀), steps)
``` ```
### B. Data Processing ### B. Data Processing
```mpl ```mpl
-- Statistical analysis -- Statistical analysis
data ← loadCSV("measurements.csv") data ← loadCSV("measurements.csv");
μ ← (Σ x ∈ data: x) ÷ |data| total ← 0;
σ ← √((Σ x ∈ data: (x - μ)²) ÷ |data|) ∀ x ∈ data : total ← total + x;
✎ "Mean: " + μ + ", StdDev: " + σ μ ← total ÷ count(data);
✎("Mean: " + μ)
``` ```
### C. Web Services ### C. Web Services
```mpl ```mpl
server ← λport: server ← λport: ∀request ∈ listen(port): (
∀request ∈ listen(port): response ← handleRequest(request);
response ← handleRequest(request) ‖ ⇀_client response
send(response) ) ‖ acceptNext();
``` ```
### D. Machine Learning ### D. Machine Learning
```mpl ```mpl
-- Neural network layer -- Neural network layer
layer ≜ λW,b,x: σ(W × x + b) σ ≜ λz: 1 ÷ (1 + exp(-z));
where σ ← λz: 1 ÷ (1 + e^(-z)) layer ≜ λW, b, x: σ(W × x + b);
``` ```
### E. Systems Programming ### E. Systems Programming
```mpl ```mpl
-- Resource management with RAII -- Resource management with RAII
processFile ← λpath: processFile ← λpath: 〔
〔file ← ⊕open(path) file ← open(path) ⊕;
data ← read(file) data ← read(file);
parse(data)〕 parse(data)
-- file automatically closed {- file automatically closed at end of 〔〕 -}
〕;
``` ```
## IX. Limitations and Future Work ## IX. Limitations and Future Work
@ -300,10 +303,10 @@ processFile ← λpath:
From parser to production: From parser to production:
1. **M1 (2025)**: REPL with basic type inference 1. **M1**: REPL with basic type inference
2. **M2 (2026)**: Compiler, standard library, IDE integration 2. **M2**: Compiler, standard library, IDE integration
3. **M3 (2027)**: Performance optimization, advanced types 3. **M3**: Performance optimization, advanced types
4. **M4 (2028)**: Production readiness, ecosystem tools 4. **M4**: Production readiness, ecosystem tools
### B. Research Directions ### B. Research Directions

48
whitepaper/mpl-whitepaper.tex
View file

@ -81,7 +81,7 @@ developtheweb@protonmail.com}}
\maketitle \maketitle
\begin{abstract} \begin{abstract}
In a school in Cairo, a 10-year-old girl named Fatima watches her teacher write a simple computer program on the board. The code is full of foreign words that might as well be magic spells to her Arabic-speaking mind. This scene repeats in classrooms worldwide, where virtually all mainstream programming languages impose English keywords as fundamental syntax, creating cognitive friction for the 80\% of humanity who don't speak English. This paper presents Mathematical Programming Language (MPL), a novel approach that replaces traditional keywords with mathematical notation—humanity's existing universal language. MPL demonstrates that a complete, production-ready programming language can be built entirely from mathematical symbols while maintaining full expressiveness across all programming paradigms. Our implementation consists of an ANTLR 4 grammar supporting over 70 Unicode mathematical operators, 24 Greek letter variables, and novel effect operators for computational effects. Through hypothetical scenarios like a student's journey from printing "Jambo!" to teaching peers within one year, we envision potential improvements in learning metrics: First Program Time could be reduced from days to minutes, retention rates might exceed traditional approaches, and teachers could enthusiastically adopt MPL in non-English classrooms. MPL proves that cognitive universality in programming languages is not just theoretically possible but practically achievable, opening a path toward truly global programming tools that transcend linguistic boundaries and enable cognitive justice in technology education. In a school in Cairo, a 10-year-old girl named Fatima watches her teacher write a simple computer program on the board. The code is full of foreign words that might as well be magic spells to her Arabic-speaking mind. This scene repeats in classrooms worldwide, where virtually all mainstream programming languages impose English keywords as fundamental syntax, creating cognitive friction for the 80\% of humanity who don't speak English. This paper presents Mathematical Programming Language (MPL), a novel approach that replaces traditional keywords with mathematical notation—humanity's existing universal language. MPL demonstrates that a programming language can be built entirely from mathematical symbols; the current milestone is a fully working parser, with execution to follow. Our implementation consists of an ANTLR 4 grammar supporting over 70 Unicode mathematical operators, 24 Greek letter variables, and novel effect operators for computational effects. Through hypothetical scenarios like a student's journey from printing "Jambo!" to teaching peers within one year, we envision potential improvements in learning metrics: First Program Time could be reduced from days to minutes, retention rates might exceed traditional approaches, and teachers could enthusiastically adopt MPL in non-English classrooms. MPL proves that cognitive universality in programming languages is not just theoretically possible but practically achievable, opening a path toward truly global programming tools that transcend linguistic boundaries and enable cognitive justice in technology education.
\end{abstract} \end{abstract}
\begin{IEEEkeywords} \begin{IEEEkeywords}
@ -223,7 +223,7 @@ MPL introduces intuitive symbols for computational concepts:
\textbf{Resources}: ⊕/⊖ (circled plus/minus) for acquire/release \textbf{Resources}: ⊕/⊖ (circled plus/minus) for acquire/release
These symbols were chosen through extensive testing with educators and children, ensuring each passes the Fatima Test. These symbols were chosen to pass the Fatima Test; empirical validation with educators and children is planned, not yet performed.
\subsection{Real Code Examples} \subsection{Real Code Examples}
@ -236,9 +236,9 @@ Here's "Hello World" in MPL – as simple as a hypothetical student's first prog
A more complex example calculating rectangle area: A more complex example calculating rectangle area:
\begin{lstlisting}[language=MPL] \begin{lstlisting}[language=MPL]
ℓ ← 5 L ← 5;
w ← 3 w ← 3;
A ← ℓ × w A ← L × w;
✎ A ✎ A
\end{lstlisting} \end{lstlisting}
@ -246,11 +246,11 @@ A ← ℓ × w
\subsection{Technical Architecture} \subsection{Technical Architecture}
The MPL implementation consists of an ANTLR 4 grammar spanning 373 lines defining complete syntax, Unicode normalization ensuring é and é are treated identically, ASCII fallbacks where every symbol has text escapes (λ → \texttt{\textbackslash lambda}), and multi-platform support running on any Unicode-capable system. The MPL implementation consists of an ANTLR 4 grammar defining the complete M0 syntax, ASCII fallbacks where every symbol has exactly one text escape (λ → \texttt{\textbackslash lambda}), and multi-platform support running on any Unicode-capable system. Unicode NFC normalization is planned.
\subsection{Parser Validation} \subsection{Parser Validation}
Validation shows zero ambiguities across all test programs, a 12-level precedence hierarchy matching mathematical conventions, round-trip testing between Unicode and ASCII forms, and testing on example programs. Continuous integration enforces that the grammar compiles with zero ANTLR errors and zero warnings, that all ten example programs parse, and that every MPL code block in the project documentation parses. The precedence chain is documented in \texttt{precedence.csv}.
\section{Evaluation} \section{Evaluation}
@ -265,16 +265,16 @@ To illustrate MPL's potential impact, consider a hypothetical student's progress
\textbf{Month 3}: She calculates areas using familiar math notation: \textbf{Month 3}: She calculates areas using familiar math notation:
\begin{lstlisting}[language=MPL] \begin{lstlisting}[language=MPL]
ℓ ← 5 L ← 5;
w ← 3 w ← 3;
A ← ℓ × w A ← L × w;
✎ A ✎ A
\end{lstlisting} \end{lstlisting}
\textbf{Month 6}: A student might master loops using mathematical notation: \textbf{Month 6}: A student might master loops using mathematical notation:
\begin{lstlisting}[language=MPL] \begin{lstlisting}[language=MPL]
Σ ← 0 total ← 0;
∀ n ∈ [1..10]: Σ ← Σ + n ∀ n ∈ [1, 2, 3, 4, 5] : total ← total + n
\end{lstlisting} \end{lstlisting}
\textbf{Month 12}: A student could teach younger students, forming a coding club. The potential transformation: from novice to mentor in one year. \textbf{Month 12}: A student could teach younger students, forming a coding club. The potential transformation: from novice to mentor in one year.
@ -295,26 +295,28 @@ MPL's mathematical syntax proves powerful across domains:
\subsection{Scientific Computing} \subsection{Scientific Computing}
\begin{lstlisting}[language=MPL] \begin{lstlisting}[language=MPL]
-- Numerical integration -- Fixed-step numerical integration (Euler method)
integrate ≜ λf,a,b,n: euler ≜ λf, y, t, h, steps: ∀step∈countTo(steps): (
h ← (b - a) ÷ n y ← y + h × f(t, y);
Σ i ∈ [0..n]: t ← t + h
xi ← a + i × h );
f(xi) × h
\end{lstlisting} \end{lstlisting}
\subsection{Data Processing} \subsection{Data Processing}
\begin{lstlisting}[language=MPL] \begin{lstlisting}[language=MPL]
-- Statistical analysis -- Statistical analysis
μ ← (Σ x ∈ data: x) ÷ |data| total ← 0;
σ ← √((Σ x ∈ data: (x-μ)²) ÷ |data|) ∀ x ∈ data : total ← total + x;
μ ← total ÷ count(data);
✎("Mean: " + μ)
\end{lstlisting} \end{lstlisting}
\subsection{Web Services} \subsection{Web Services}
\begin{lstlisting}[language=MPL] \begin{lstlisting}[language=MPL]
server ← λport: server ← λport: ∀request ∈ listen(port): (
∀req ∈ listen(port): response ← handleRequest(request);
handleRequest(req) ‖ ⇀_client response
) ‖ acceptNext();
\end{lstlisting} \end{lstlisting}
\section{Limitations and Future Work} \section{Limitations and Future Work}