git @ Cat's Eye Technologies Exanoke / 6ce9f01
Make syntax somewhat less bizarre. Explain critical arguments. catseye 12 years ago
1 changed file(s) with 104 addition(s) and 71 deletion(s). Raw diff Collapse all Expand all
+104
-71
README.markdown less more
1616
1717 * You can statically analyze the bastard, and prove that all of its
1818 loops eventually terminate, and so forth; or
19 * You can write it in a language which naturally restricts you to the
20 primitive recursive functions.
19 * You can write it in a language which is inherently restricted to
20 expressing only primitive recursive functions.
2121
2222 The second option is the route [PL-{GOTO}][] takes. But that's an imperative
2323 language, and it's fairly easy to restrict an imperative language in this
3737 primitive recursive functions? It *should* be possible... and easier than
3838 statically analyzing an arbitrary program... but it's not immediately trivial.
3939 Functional languages don't do the `for` loop thing, they do the recursion
40 thing, and there are no natural bound on recursion, and they would have
40 thing, and there are no natural bounds on that recursion, so those would have
4141 to be embodied by the grammar, and... well, it sounds interesting, but
4242 doable. So let's try it.
4343
5454
5555 * It doesn't perform mutual recursion.
5656 * When recursion happens, it's always with arguments that are strictly
57 "smaller" than the arguments the function received.
58 * There is always a base case to the recursion, so that it always
57 "smaller" values than the arguments the function received.
58 * There is a "smallest" value that an argument can take on, so that
59 there is always a base case to the recursion, so that it always
5960 eventually terminates.
6061 * Higher-order functions are not used.
6162
6869 "smallerness". (Gee, typing that made me feel a bit like George W. Bush!)
6970
7071 The third point can be enforced by providing some default behaviour when
71 functions are called with the "smallest" kinds of values.
72 functions are called with the "smallest" kinds of values. This could be
73 as simple as terminating the program if you try to find a value "smaller"
74 than the "smallest" value.
7275
7376 The fourth point can be enforced by simply disallowing functions to be
7477 passed to, or returned from, functions.
7578
76 TODO explain critical arguments and how the only critical argument in
77 an Exanoke function is always the first argument.
79 ### Note on Critical Arguments ###
80
81 I should note, though, that the second point is an oversimplification.
82 Not *all* arguments need to be strictly "smaller" upon recursion -- only
83 those arguments which are used to determine *if* the function recurses.
84 I'll call those the _critical arguments_. Other arguments can take on
85 any value (which is useful for having "accumulator" arguments and such.)
86
87 When statically analyzing a function for primitive recursive-ness, you
88 need to check how it decides to rescurse, to find out which arguments are
89 the critical arguments, so you can check that those ones always get
90 "smaller".
91
92 But we can proceed in a simpler fashion here -- we can simply say that
93 the first argument to every function is the critical argument, and all
94 the rest aren't. I believe this is without loss of generality, as we can
95 always split some functionality which would require more than one critical
96 argument across multiple functions, each of which only has one critical
97 argument. (Much like every `for` loop has only one loop variable.)
7898
7999 Data types
80100 ----------
85105 the second element of each pair, and `NIL` is the agreed-upon list-terminating
86106 atom, much love to it.)
87107
88 Arguments do not have user-defined names, they're just referred to strings of
89 `#` symbols: `#` is the first argument to the function, `##` is the second,
90 etc. When a function is defined, the name of the last argument is given, to
91 specify how many arguments the function takes.
92
93108 Grammar
94109 -------
95110
96111 Exanoke ::= {FunDef} Expr.
97 FunDef ::= "def" name<lowercase> "(" FirstArg | Arg ")" Expr.
98 FirstArg ::= "#".
99 Arg ::= "##" {"#"}.
100 Expr ::= "cons" "(" Expr Expr ")"
112 FunDef ::= "def" name<lowercase> "(" "#" {"," Arg} ")" Expr.
113 Arg ::= name<lowercase>.
114 Expr ::= "cons" "(" Expr "," Expr ")"
101115 | "if" Expr "then" Expr "else" Expr
102 | "self" "(" Smaller {Expr} ")"
103 | "eq?" "(" Expr Expr")"
104 | "cons?" Expr
105 | "not" Expr
116 | "self" "(" Smaller {"," Expr} ")"
117 | "eq?" "(" Expr "," Expr")"
118 | "cons?" "(" Expr ")"
119 | "not" "(" Expr ")"
106120 | "(" Expr ")"
107 | name<lowercase> "(" {Expr} ")"
108 | FirstArg
121 | name<lowercase> "(" Expr {"," Expr} ")"
122 | "#"
109123 | Arg
110124 | Atom
111125 | Smaller.
116130 | FirstArg.
117131 Atom ::= name<uppercase>.
118132
119 TODO still not entirely sure about `<if`.
133 The first argument to a function does not have a user-defined name; it is
134 simply referred to as `#`.
135
136 The names of arguments defined in a function shall not shadow the names of
137 any previously-defined functions.
138
139 Note that `<if` does not seem to be truly necessary. Its only use is to embed
140 a conditional into the first argument being passed to a recursive call. You
141 could also use a regular `if` and make the recursive call in both branches,
142 one with `TRUE` as the first argument and the other with `FALSE`. I think.
120143
121144 Examples
122145 --------
123146
124 | cons(HI THERE)
147 | cons(HI, THERE)
125148 = (HI THERE)
126149
127 | (cons(HI cons(THERE NIL)))
150 | (cons(HI, cons(THERE, NIL)))
128151 = (HI (THERE NIL))
129152
130 | <head cons(HI THERE)
153 | <head cons(HI, THERE)
131154 = HI
132155
133 | <tail cons(HI THERE)
156 | <tail cons(HI, THERE)
134157 = THERE
135158
136 | <tail <tail (cons(HI cons(THERE NIL)))
159 | <tail <tail (cons(HI, cons(THERE, NIL)))
137160 = NIL
138161
139162 | <tail FOO
140 ? Not a cons cell
163 ? tail: Not a cons cell
141164
142165 | <head BAR
143 ? Not a cons cell
166 ? head: Not a cons cell
144167
145168 | if TRUE then HI else THERE
146169 = HI
148171 | if HI then HERE else THERE
149172 = THERE
150173
151 | eq?(HI THERE)
174 | eq?(HI, THERE)
152175 = FALSE
153176
154 | eq?(HI HI)
177 | eq?(HI, HI)
155178 = TRUE
156179
157 | cons? HI
180 | cons?(HI)
158181 = FALSE
159182
160 | cons? cons(WAGGA NIL)
183 | cons?(cons(WAGGA, NIL))
161184 = TRUE
162185
163 | not TRUE
186 | not(TRUE)
164187 = FALSE
165188
166 | not FALSE
189 | not(FALSE)
167190 = TRUE
168191
169 | not cons(WANGA NIL)
192 | not(cons(WANGA, NIL))
170193 = TRUE
171194
172195 | #
182205
183206 | def id(#)
184207 | #
185 | id(FOO BAR)
208 | id(FOO, BAR)
186209 ? Arity mismatch
187210
188211 | def id(#)
190213 | id(WOO)
191214 ? Arity mismatch
192215
193 | def snd(##)
194 | ##
195 | snd(FOO BAR)
216 | def snd(#, another)
217 | another
218 | snd(FOO, BAR)
196219 = BAR
197220
198 | def snd(##)
199 | ##
221 | def snd(#, another)
222 | another
200223 | snd(FOO)
201224 ? Arity mismatch
202225
203 | def snoc(##)
204 | cons(## #)
226 | def snoc(#, another)
227 | cons(another, #)
205228 | snoc(THERE HI)
206229 = (HI THERE)
207230
208231 | def count(#)
209232 | self(<tail #)
210 | count(cons(A cons(B NIL)))
211 ? Not a cons cell
233 | count(cons(A, cons(B, NIL)))
234 ? tail: Not a cons cell
212235
213236 | def count(#)
214 | if eq?(# NIL) then NIL else self(<tail #)
215 | count(cons(A cons(B NIL)))
237 | if eq?(#, NIL) then NIL else self(<tail #)
238 | count(cons(A, cons(B, NIL)))
216239 = NIL
217240
218241 | def last(#)
220243 | last(cons(A cons(B GRAAAP)))
221244 = GRAAAP
222245
223 | def count(##)
224 | if eq?(# NIL) then ## else self(<tail # cons(ONE ##))
225 | count(cons(A cons(B NIL)) NIL)
246 | def count(#, acc)
247 | if eq?(#, NIL) then ## else self(<tail #, cons(ONE, acc))
248 | count(cons(A, cons(B, NIL)), NIL)
226249 = (ONE (ONE NIL))
227250
228251 | def double(#)
229 | cons(# #)
252 | cons(#, #)
230253 | def quadruple(#)
231254 | double(double(#))
232 | quadruple MEOW
255 | quadruple(MEOW)
233256 = ((MEOW MEOW) (MEOW MEOW))
234257
235258 | def quadruple(#)
236259 | double(double(#))
237260 | def double(#)
238 | cons(# #)
261 | cons(#, #)
239262 | MEOW
240263 ? Undefined function
241264
242265 | def urff(#)
243 | self(cons(# #))
266 | self(cons(#, #))
244267 | urff(WOOF)
245268 ? Expected <smaller>, found "cons"
246269
249272 | urff(GRAAAAP)
250273 ? Expected <smaller>, found "#"
251274
252 | def urff(##)
253 | self(##)
254 | urff(GRAAAAP SKOOOORP)
255 ? Expected <smaller>, found "##"
256
257 | def urff(##)
258 | self(<tail ##)
259 | urff(GRAAAAP SKOOOORP)
260 ? Expected <smallerterm>, found "##"
275 | def urff(#, boof)
276 | self(boof)
277 | urff(GRAAAAP, SKOOOORP)
278 ? Expected <smaller>, found "boof"
279
280 | def urff(#, boof)
281 | self(<tail boof)
282 | urff(GRAAAAP, SKOOOORP)
283 ? Expected <smallerterm>, found "boof"
261284
262285 | def urff(#)
263286 | self(WANGA)
265288 ? Expected <smaller>, found "WANGA"
266289
267290 | def urff(#)
268 | self(if eq?(self(#) A) then <head # else <tail #)
269 | urff(GRAAAAP)
270 ? Expected <smaller>, found "self"
291 | self(if eq?(A, A) then <head # else <tail #)
292 | urff(GRAAAAP)
293 ? Expected <smaller>, found "if"
294
295 | def urff(#)
296 | self(<if eq?(A, A) then <head # else <tail #)
297 | urff(GRAAAAP)
298 ? head: Not a cons cell
299
300 | def urff(#)
301 | self(<if eq?(self(<head #), A) then <head # else <tail #)
302 | urff(GRAAAAP)
303 ? head: Not a cons cell
271304
272305 | def urff(#)
273306 | self(if self(<tail #) then <head # else <tail #)
274307 | urff(cons(GRAAAAP FARRRRP))
275 ? Not a cons cell
308 ? tail: Not a cons cell
276309
277310 TODO more examples here...
278311
279312 Discussion
280313 ----------
281314
282 I don't know if this holds water yet or not.
315 I'm pretty sure this holds water, at this point.
283316
284317 The name "Exanoke" started life as a typo for the word "example".