📚 Phase 12.5 最適化戦略 & Phase 15 セルフホスティング計画
Phase 12.5: MIR15最適化戦略 - コンパイラ丸投げ作戦 - optimization-strategy.txt: 詳細戦略(MIR側は軽量、コンパイラに丸投げ) - implementation-examples.md: 具体的な実装例 - debug-safety-comparison.md: 現在のDebugBox vs ChatGPT5提案の比較分析 Phase 15: Nyashセルフホスティング - 究極の目標 - self-hosting-plan.txt: 内蔵Craneliftによる実現計画 - technical-details.md: CompilerBox設計とブートストラップ手順 - README.md: セルフホスティングのビジョン 重要な知見: - LLVM統合完了済み(Phase 11)だが依存が重すぎる - Craneliftが現実的な選択肢(3-5MB vs LLVM 50-100MB) - 「コンパイラもBox、すべてがBox」の夢へ MASTERロードマップ更新済み
This commit is contained in:
148
docs/papers/active/mir15-fullstack/chapters/02-box-theory.md
Normal file
148
docs/papers/active/mir15-fullstack/chapters/02-box-theory.md
Normal file
@ -0,0 +1,148 @@
|
||||
# Chapter 2: The Box Theory - A Mathematical Foundation
|
||||
|
||||
## 2.1 The Atomic Theory of Programming
|
||||
|
||||
Just as matter is composed of atoms that combine to form molecules and complex structures, we propose that programs can be viewed as compositions of atomic operations that combine through a universal abstraction—the Box.
|
||||
|
||||
### Definition 2.1 (Box)
|
||||
A Box B is a tuple (S, O, σ) where:
|
||||
- S is the internal state space
|
||||
- O is the set of operations {o₁, o₂, ..., oₙ}
|
||||
- σ: S × O × Args → S × Result is the state transition function
|
||||
|
||||
### Definition 2.2 (Atomic Operations)
|
||||
The minimal set of atomic operations A = {a₁, a₂, ..., a₁₅} forms the complete basis for computation:
|
||||
|
||||
```
|
||||
A = {Const, UnaryOp, BinOp, Compare, TypeOp,
|
||||
Load, Store, Branch, Jump, Return, Phi,
|
||||
NewBox, BoxCall, ArrayGet, ArraySet, ExternCall}
|
||||
```
|
||||
|
||||
## 2.2 Composition and Recursion
|
||||
|
||||
The power of the Box Theory lies not in the individual operations but in their composition:
|
||||
|
||||
### Theorem 2.1 (Compositional Completeness)
|
||||
For any computable function f, there exists a finite composition of Boxes B₁, B₂, ..., Bₙ such that f can be expressed using only operations from A.
|
||||
|
||||
*Proof sketch*: By showing that A contains operations for:
|
||||
1. Value creation (Const, NewBox)
|
||||
2. State manipulation (Load, Store, ArrayGet, ArraySet)
|
||||
3. Control flow (Branch, Jump, Return, Phi)
|
||||
4. Composition (BoxCall)
|
||||
5. External interaction (ExternCall)
|
||||
|
||||
We can construct any Turing-complete computation.
|
||||
|
||||
### Lemma 2.1 (Recursive Box Construction)
|
||||
Boxes can contain other Boxes, enabling recursive composition:
|
||||
|
||||
```
|
||||
GuiBox = Box({
|
||||
WindowBox,
|
||||
ButtonBox,
|
||||
CanvasBox
|
||||
})
|
||||
```
|
||||
|
||||
This recursive nature allows unbounded complexity from bounded primitives.
|
||||
|
||||
## 2.3 The Box Calculus
|
||||
|
||||
We formalize Box operations using a simple calculus:
|
||||
|
||||
### Syntax
|
||||
```
|
||||
e ::= x (variable)
|
||||
| c (constant)
|
||||
| new B(e₁,...,eₙ) (box creation)
|
||||
| e.m(e₁,...,eₙ) (box method call)
|
||||
| e₁ ⊕ e₂ (binary operation)
|
||||
| if e₁ then e₂ else e₃ (conditional)
|
||||
```
|
||||
|
||||
### Operational Semantics
|
||||
|
||||
**Box Creation**:
|
||||
```
|
||||
σ ⊢ eᵢ ⇓ vᵢ (for i = 1..n)
|
||||
________________________________
|
||||
σ ⊢ new B(e₁,...,eₙ) ⇓ ref(B, v₁,...,vₙ)
|
||||
```
|
||||
|
||||
**Method Call**:
|
||||
```
|
||||
σ ⊢ e ⇓ ref(B, state) σ ⊢ eᵢ ⇓ vᵢ
|
||||
B.m(state, v₁,...,vₙ) → (state', result)
|
||||
_________________________________________
|
||||
σ ⊢ e.m(e₁,...,eₙ) ⇓ result
|
||||
```
|
||||
|
||||
## 2.4 From Theory to Practice
|
||||
|
||||
The Box Theory manifests in Nyash through concrete examples:
|
||||
|
||||
### Example 2.1 (GUI as Boxes)
|
||||
```nyash
|
||||
box Button from Widget {
|
||||
init { text, onClick }
|
||||
|
||||
render() {
|
||||
# Rendering is just Box operations
|
||||
return me.drawRect(me.bounds)
|
||||
.drawText(me.text)
|
||||
}
|
||||
|
||||
handleClick(x, y) {
|
||||
if me.contains(x, y) {
|
||||
me.onClick()
|
||||
}
|
||||
}
|
||||
}
|
||||
```
|
||||
|
||||
Every GUI element is a Box, every interaction is a BoxCall. The 15 atomic operations suffice because complexity resides in Box composition, not in the instruction set.
|
||||
|
||||
### Example 2.2 (Concurrency as Boxes)
|
||||
```nyash
|
||||
box TaskGroup {
|
||||
spawn(target, method, args) {
|
||||
# Concurrency through Box abstraction
|
||||
local future = new FutureBox()
|
||||
ExternCall("scheduler", "enqueue", [target, method, args, future])
|
||||
return future
|
||||
}
|
||||
}
|
||||
```
|
||||
|
||||
## 2.5 Why 15 Instructions Suffice
|
||||
|
||||
The key insight is the separation of concerns:
|
||||
|
||||
1. **Structure** (MIR): Handles control flow and basic operations
|
||||
2. **Behavior** (Boxes): Encapsulates domain-specific complexity
|
||||
3. **Composition** (BoxCall): Enables unlimited combinations
|
||||
|
||||
This separation allows us to keep the structural layer (MIR) minimal while achieving arbitrary functionality through behavioral composition.
|
||||
|
||||
### Theorem 2.2 (Minimality)
|
||||
The 15-instruction set A is minimal in the sense that removing any instruction would break either:
|
||||
1. Turing completeness
|
||||
2. Practical usability
|
||||
3. Box abstraction capability
|
||||
|
||||
## 2.6 Implications
|
||||
|
||||
The Box Theory has profound implications:
|
||||
|
||||
1. **Language Design**: Complexity should be in libraries, not in the core language
|
||||
2. **Implementation**: Simpler IRs can lead to more robust implementations
|
||||
3. **Optimization**: Focus on Box boundaries rather than instruction-level optimization
|
||||
4. **Education**: Minimal languages are easier to learn and understand
|
||||
|
||||
## 2.7 Conclusion
|
||||
|
||||
The Box Theory provides a mathematical foundation for building complex systems from minimal primitives. By viewing computation as the composition of atomic operations through Box abstractions, we can achieve the seemingly impossible: full-stack applications, including GUI programs, with just 15 instructions.
|
||||
|
||||
This is not merely a theoretical exercise—as we will show in the following chapters, this theory has been successfully implemented and validated in the Nyash programming language.
|
||||
Reference in New Issue
Block a user