Skip to content

Commit deb756f

Browse files
RIvanceRIvance
committed
docs: add formal proof
1 parent 69f0770 commit deb756f

File tree

12 files changed

+965
-267
lines changed

12 files changed

+965
-267
lines changed

‎.gitignore‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -2,6 +2,7 @@
22
_build/
33
site/
44
.vscode/
5+
.idea/
56
.DS_Store
67
.env
78
.well-known/

docs/Keywords and Identifiers.md renamed to docs/01-keywords.md

Lines changed: 34 additions & 34 deletions
Original file line numberDiff line numberDiff line change
@@ -4,42 +4,42 @@
44

55
Saki supports following keywords:
66

7-
| Keyword | Description |
8-
| -------------------- | ------------------------------------------------------------ |
9-
| `import` | Module import |
10-
| `pub` | Public modifier |
11-
| `def` | Function definition |
12-
| `impl` | Implementation block |
13-
| `operator` | Operator declaration |
14-
| `prefix` | Prefix modifier (unary operator) |
15-
| `postfix` | Postfix modifier (unary operator) |
16-
| `left-assoc` | Left association modifier (binary operator) |
17-
| `right-assoc` | Right association modifier (binary operator) |
18-
| `tighter-than` | Precedence partial-order modifier (binary operator) |
19-
| `looser-than` | Precedence partial-order modifier (binary operator) |
20-
| `same-as` | Precedence partial-order modifier (binary operator) |
21-
| `let` | Let binding |
22-
| `instance` | Instance value |
23-
| `enum` | Enum type (Algebraic Data Type) |
24-
| `record` | Record type |
25-
| `universe` | Universe |
26-
| `self` | Self instance |
27-
| `Self` | Self type |
7+
| Keyword | Description |
8+
|----------------------|------------------------------------------------------------------|
9+
| `import` | Module import |
10+
| `pub` | Public modifier |
11+
| `def` | Function definition |
12+
| `impl` | Implementation block |
13+
| `operator` | Operator declaration |
14+
| `prefix` | Prefix modifier (unary operator) |
15+
| `postfix` | Postfix modifier (unary operator) |
16+
| `left-assoc` | Left association modifier (binary operator) |
17+
| `right-assoc` | Right association modifier (binary operator) |
18+
| `tighter-than` | Precedence partial-order modifier (binary operator) |
19+
| `looser-than` | Precedence partial-order modifier (binary operator) |
20+
| `same-as` | Precedence partial-order modifier (binary operator) |
21+
| `let` | Let binding |
22+
| `instance` | Instance value |
23+
| `enum` | Enum type (Algebraic Data Type) |
24+
| `record` | Record type |
25+
| `universe` | Universe |
26+
| `self` | Self instance |
27+
| `Self` | Self type |
2828
| `this` | Current subject (such as recursive access in anonymous function) |
29-
| `forall` / `Π` / `∀` | Forall / dependent pi type |
30-
| `exists` / `Σ` / `∃` | Exists / dependent sigma type |
31-
| `if` | If-expression |
32-
| `then` | Then branch in if-expression |
33-
| `else` | Else branch in if-expression |
34-
| `match` | Match-expression |
35-
| `case` | Case clause in match-expression |
29+
| `forall` / `Π` / `∀` | Forall / dependent pi type |
30+
| `exists` / `Σ` / `∃` | Exists / dependent sigma type |
31+
| `if` | If-expression |
32+
| `then` | Then branch in if-expression |
33+
| `else` | Else branch in if-expression |
34+
| `match` | Match-expression |
35+
| `case` | Case clause in match-expression |
3636

3737
## Identifiers
3838

39-
| Identifier | Example | Description |
40-
| :----------------------------------------------------------: | :------------------------------: | :-----------------------------------------------: |
39+
| Identifier | Example | Description |
40+
|:----------------------------------------------------------------------------:|:--------------------------------:|:-------------------------------------------------:|
4141
| `camelCaseWithEnglishOrGreekLetters` / `withOptionalPostfixSingleQuotation'` | `value`, `α`, `παράδειγμα`, `n'` | Values |
42-
| `PascalCaseInEnglish` / A single blackboard bold letter | `Nat`, `ℕ` | Types |
43-
| `'PascalCaseWithAPrefixedSingleQuotation` | `'Type`, `'Runnable` | Contract universes |
44-
| `#Universe` | `#Universe` | The universe that all contract universes lives in |
45-
| `'Type_n` / `'Typeₙ` | `'Type_3`, `'Type₃` | Higher-level universes |
42+
| `PascalCaseInEnglish` / A single blackboard bold letter | `Nat`, `ℕ` | Types |
43+
| `'PascalCaseWithAPrefixedSingleQuotation` | `'Type`, `'Runnable` | Contract universes |
44+
| `#Universe` | `#Universe` | The universe that all contract universes lives in |
45+
| `'Type_n` / `'Typeₙ` | `'Type_3`, `'Type₃` | Higher-level universes |

docs/Martin-Löf Type Theory.md renamed to docs/02-mltt.md

Lines changed: 10 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -1,3 +1,5 @@
1+
# Martin-Löf Type Theory
2+
13
<script type="module" src="/javascripts/editor.js"></script>
24
<link rel="stylesheet" href="/static/styles.css">
35

@@ -28,7 +30,7 @@ MLTT extends this correspondence by incorporating dependent types, allowing for
2830
**Formation Rule**:
2931

3032
$$
31-
\frac{\Gamma \vdash A \ \text{type} \quad \Gamma, x : A \vdash B(x) : \mathcal{U}}{\Gamma \vdash \Pi(x : A) . B(x) : \mathcal{U}}
33+
\frac{\Gamma \vdash A : \mathcal{U} \quad \Gamma, x : A \vdash B(x) : \mathcal{U}}{\Gamma \vdash \Pi(x : A) . B(x) : \mathcal{U}}
3234
$$
3335

3436
**Introduction Rule**:
@@ -157,6 +159,7 @@ type Type = Value
157159

158160
*Neutral values*, however, represent terms that are blocked from further reduction due to free variables or unsolved dependencies. Neutral values allow terms with unresolved components to be stored without forcing premature reductions. They are especially significant in representing expressions that cannot simplify further because they involve variables that are free in the current context.
159161
<div class="code-editor">
162+
160163
```
161164
type NeutralValue = inductive {
162165
// Variable: A neutral value representing an unresolved variable.
@@ -297,19 +300,19 @@ In formal terms, NBE employs structured definitions of evaluation and applicatio
297300

298301
#### Evaluation Rules
299302
$$
300-
\llbracket x \rrbracket_{\rho} = \rho(x)
303+
⟦ x ⟧_{\rho} = \rho(x)
301304
$$
302305

303306
For a variable $x$, evaluation retrieves $x$'s value from the environment $\rho$.
304307

305308
$$
306-
\llbracket \lambda x.t \rrbracket_{\rho} = (\rho, \lambda x.t)
309+
⟦ \lambda x.t ⟧_{\rho} = (\rho, \lambda x.t)
307310
$$
308311

309312
A lambda function evaluates to a closure with $\rho$ capturing the environment.
310313

311314
$$
312-
\llbracket t \ u \rrbracket_{\rho} = \llbracket t \rrbracket_{\rho} \cdot \llbracket u \rrbracket_{\rho}
315+
⟦ t \ u ⟧_{\rho} = ⟦ t ⟧_{\rho} \cdot ⟦ u ⟧_{\rho}
313316
$$
314317

315318
Application proceeds by evaluating both the function $t$ and argument $u$.
@@ -318,7 +321,7 @@ Application proceeds by evaluating both the function $t$ and argument $u$.
318321
Application between values distinguishes between closures and neutral values:
319322

320323
$$
321-
(\rho, \lambda x.t) \cdot v = \llbracket t \rrbracket_{\rho[x \mapsto v]}
324+
(\rho, \lambda x.t) \cdot v = ⟦ t ⟧_{\rho[x \mapsto v]}
322325
$$
323326
If the function is a closure, the argument $v$ extends the environment.
324327

@@ -622,8 +625,8 @@ def readBack(value: Value, env: Env): Term = match value {
622625
* @return The universe level as an `Int`.
623626
*/
624627
def universeLevel(ty: Type): Int = match ty {
625-
case Value::Type(univ) => univ // Extract universe level.
626-
case _ => panic("Failed to unwrap universe level: not a type") // Panic if not a type.
628+
case Value::Type(univ) => univ
629+
case _ => panic("Failed to unwrap universe level: not a type")
627630
}
628631
629632
/**

0 commit comments

Comments
 (0)