Skip to content

Commit 607788c

Browse files
oderskyodersky
committed
A simplified calculus
with a sketch of its meta theory.
1 parent 53e6d67 commit 607788c

File tree

1 file changed

+229
-0
lines changed

1 file changed

+229
-0
lines changed

‎docs/docs/reference/simple-smp.md

Lines changed: 229 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,229 @@
1+
# Simple Symmetric Metaprogramming
2+
3+
23.12.2017
4+
5+
This note presents a simplified variant of symmetric metaprogramming
6+
which only treats dialgogues between two stages. We could have quotes
7+
containing splices (which can contain quotes, which can contain
8+
splices, and so on). Or we could start with a splice with embedded
9+
quotes. The important restriction is that (1) a term contains toplevel
10+
quotes or toplevel splices, but not both and (2) quotes cannot appear
11+
directly inside quotes and splices cannot appear directly inside
12+
splices. In other words, the universe is restricted to two phases
13+
only.
14+
15+
Under this restriction we can simplify the typing rules so that there are
16+
always exactly two environments instead of having a stack of environments.
17+
The variant presented here differs from the full calculus also in that we
18+
replace evaluation contexts with contextual typing rules. While this
19+
is more verbose, it makes it easier to set up the meta theory.
20+
21+
## Syntax
22+
23+
Terms t ::= x variable
24+
(x: T) => t lambda
25+
t t application
26+
’t quote
27+
~t splice
28+
29+
Simple terms u ::= x | (x: T) => u | u u
30+
31+
Values v ::= (x: T) => t lambda
32+
’u quoted value
33+
34+
Types T ::= A base type
35+
T -> T function type
36+
’T quoted type
37+
38+
## Operational semantics:
39+
40+
### Evaluation:
41+
42+
((x: T) => t) v --> [x := v]t
43+
44+
t1 --> t2
45+
---------------
46+
t1 t --> t2 t
47+
48+
t1 --> t2
49+
---------------
50+
v t1 --> v t2
51+
52+
t1 ==> t2
53+
-------------
54+
’t1 --> ’t2
55+
56+
57+
### Splicing:
58+
59+
~’u ==> u
60+
61+
t1 ==> t2
62+
-------------------------------
63+
(x: T) => t1 ==> (x: T) => t2
64+
65+
t1 ==> t2
66+
---------------
67+
t1 t ==> t2 t
68+
69+
t1 ==> t2
70+
---------------
71+
u t1 ==> u t2
72+
73+
t1 --> t2
74+
-------------
75+
~t1 ==> ~t2
76+
77+
78+
## Typing rules:
79+
80+
Typing judgments are of the form `E1 * E2 |- t: T` where `E1, E2` are environments and
81+
`*` is one of `~` and `’`.
82+
83+
x: T in E2
84+
---------------
85+
E1 * E2 |- x: T
86+
87+
88+
E1 * E2, x: T1 |- t: T2
89+
--------------------------------
90+
E1 * E2 |- (x: T1) => t: T -> T2
91+
92+
93+
E1 * E2 |- t1: T2 -> T E1 * E2 |- t2: T2
94+
-------------------------------------------
95+
E1 * E2 |- t1 t2: T
96+
97+
98+
E1 ’ E2 |- t: T
99+
-----------------
100+
E1 ~ E2 |- ’t: ’T
101+
102+
103+
E1 ~ E2 |- t: ’T
104+
----------------
105+
E1 ’ E2 |- ~t: T
106+
107+
108+
(Curiously, this looks a bit like a Christmas tree).
109+
110+
## Soundness
111+
112+
The meta-theory typically requires mutual inductions over two judgements.
113+
114+
__Progress Theorem__:
115+
116+
1. If `E1 ~ |- t: T` then either `t = v` for some value `v` or `t --> t2` for some term `t2`.
117+
2. If ` ’ E2 |- t: T` then either `t = u` for some simple term `u` or `t ==> t2` for some term `t2`.
118+
119+
Proof by structural induction over terms.
120+
121+
To prove (1):
122+
123+
- the cases for variables, lambdas and applications are as in STL.
124+
- If `t = ’t2`, then by inversion we have ` ’ E1 |- t2: T2` for some type `T2`.
125+
By second I.H., we have one of:
126+
- `t2 = u`, hence `’t2` is a value,
127+
- `t2 ==> t3`, hence `’t2 --> ’t3`.
128+
- The case `t = ~t2` is not typable.
129+
130+
To prove (2):
131+
132+
- If `t = x` then `t` is a simple term.
133+
- If `t = (x: T) => t2`, then either `t2` is a simple term, in which case `t` is as well.
134+
Or by the second I.H. `t2 ==> t3`, in which case `t ==> (x: T) => t3`.
135+
- If `t = t1 t2` then one of three cases applies:
136+
137+
- `t1` and `t2` are a simple term, then `t` is as well a simple term.
138+
- `t1` is not a simple term. Then by the second IH, `t1 ==> t12`, hence `t ==> t12 t2`.
139+
- `t1` is a simple term but `t2` is not. Then by the second IH. `t2 ==> t22`, hence `t ==> t1 t22`.
140+
141+
- The case `t = ’t2` is not typable.
142+
- If `t = ~t2` then by inversion we have `E2 ~ |- t2: ’T2`, for some some type `T2`.
143+
By the first I.H., we have one of
144+
145+
- `t2 = v`. Since `t2: ’T2`, we must have `v = ’u`, for some simple term `u`, hence `t = ~’u`.
146+
By quote-splice reduction, `t ==> u`.
147+
- `t2 --> t3`. Then by the context rule for `’t`, `t ==> ’t3`.
148+
149+
150+
__Substitution Lemma__:
151+
152+
1. If `E1 ~ E2 |- s: S` and `E1 ~ E2, x: S |- t: T` then `E1 ~ E2 |- [x := s]t: T`.
153+
2. If `E1 ’ E2 |- s: S` and `E2, x: S ’ E1 |- t: T` then `E2 ’ E1 |- [x := s]t: T`.
154+
155+
The proofs are by induction on typing derivations for `t`, analogous
156+
to the proof for STL (with (2) a bit simpler than (1) since we do not
157+
need to swap lambda bindings with the bound variable `x`). The
158+
arguments that link the two hypotheses are as follows.
159+
160+
To prove (1), let `t = ’t1`. Then `T = ’T1` for some type `T1` and the last typing rule is
161+
162+
E2, x: S ’ E1 |- t1: T1
163+
-------------------------
164+
E1 ~ E2, x: S |- ’t1: ’T1
165+
166+
By the second I.H. `E2 ’ E1 |- [x := s]t1: T1`. By typing, `E1 ~ E2 |- ’[x := s]t1: ’T1`.
167+
Since `[x := s]t = [x := s](’t1) = ’[x := s]t1` we get `[x := s]t: ’T1`.
168+
169+
To prove (2), let `t = ~t1`. Then the last typing rule is
170+
171+
E1 ~ E2, x: S |- t1: ’T
172+
-----------------------
173+
E2, x: S ’ E1 |- ~t1: T
174+
175+
By the first I.H., `E1 ~ E2 |- [x := s]t1: ’T`. By typing, `E2 ’ E1 |- ~[x := s]t1: T`.
176+
Since `[x := s]t = [x := s](~t1) = ~[x := s]t1` we get `[x := s]t: T`.
177+
178+
179+
__Preservation Theorem__:
180+
181+
1. If `E1 ~ E2 |- t1: T` and `t1 --> t2` then `E1 ~ E2 |- t2: T`.
182+
2. If `E1 ’ E2 |- t1: T` and `t1 ==> t2` then `E1 ’ E2 |- t2: T`.
183+
184+
The proof is by structural induction on evaluation derivations. The proof of (1) is analogous
185+
to the proof for STL, using the substitution lemma for the beta reduction case, with the addition of reduction of quoted terms, which goes as follows:
186+
187+
- Assume the last rule was
188+
189+
t1 ==> t2
190+
-------------
191+
’t1 --> ’t2
192+
193+
By inversion of typing rules, we must have `T = ’T1` for some type `T1` such that `t1: T1`.
194+
By the second I.H., `t2: T1`, hence `’t2: `T1`.
195+
196+
197+
To prove (2):
198+
199+
- Assume the last rule was `~’u ==> u`. The typing proof of `~’u` must have the form
200+
201+
202+
E1 ’ E2 |- u: T
203+
-----------------
204+
E1 ~ E2 |- ’u: ’T
205+
-----------------
206+
E1 ’ E2 |- ~’u: T
207+
208+
Hence, `E1 ’ E2 |- u: T`.
209+
210+
- Assume the last rule was
211+
212+
t1 ==> t2
213+
-------------------------------
214+
(x: S) => t1 ==> (x: T) => t2
215+
216+
By typing inversion, `E1 ' E2, x: S |- t1: T1` for some type `T1` such that `T = S -> T1`.
217+
By the I.H, `t2: T1`. By the typing rule for lambdas the result follows.
218+
219+
- The context rules for applications are equally straightforward.
220+
221+
- Assume the last rule was
222+
223+
t1 ==> t2
224+
-------------
225+
~t1 ==> ~t2
226+
227+
By inversion of typing rules, we must have `t1: ’T`.
228+
By the first I.H., `t2: ’T`, hence `~t2: T`.
229+

0 commit comments

Comments
 (0)