Files
hakorune/docs/papers/active/paper-a-mir13-ir-design/chapters/02-box-theory.md

148 lines
4.8 KiB
Markdown
Raw Normal View History

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