git @ Cat's Eye Technologies Lariat / c623b63
Add example of searching for reducible subterm and reducing it. Chris Pressey 3 years ago
1 changed file(s) with 81 addition(s) and 51 deletion(s). Raw diff Collapse all Expand all
+81
-51
README.md less more
99 this abstract data type, and possibly variations on it, in various
1010 programming languages.
1111
12 The version of the Lariat abstract data type defined by this document
13 is version 0.1. To be promoted to 1.0 once vetted sufficiently.
12 The version of the Lariat defined by this document is 0.1. This
13 version number will be promoted to 1.0 once vetted sufficiently.
1414
1515 #### Table of Contents
1616
1818 * [The Operations](#the-operations)
1919 * [Stepping Back](#stepping-back)
2020 * [Some Examples](#some-examples)
21 * [Discussion](#discussion)
2221
2322 Background
2423 ----------
6867 > **Note**: A free variable is a term; it can be passed to any operation
6968 > that expects a term.
7069
71 ### `app(t1: term, t2: term): term`
72
73 Given a term _t1_ and a term _t2_, return an _application term_
74 which contains _t1_ as its first subterm and _t2_ as its second
70 ### `app(t: term, u: term): term`
71
72 Given a term _t_ and a term _u_, return an _application term_
73 which contains _t_ as its first subterm and _u_ as its second
7574 subterm.
7675
7776 > **Note**: An application term is a term that is an
9190 > the abstraction term to which variables are bound, is
9291 > the term returned by the operation.
9392
94 ### `resolve(t1: term, t2: term): term`
95
96 Given a term _t1_ and a term _t2_, return either _t1_ (if _t1_ is
97 not an abstraction term) or _t1'_, where _t1'_ is a version of
98 _t1_ where all bound variables in _t1'_ that were bound to _t1_
99 itself have been replaced by _t2_.
93 > **Note**: an abstraction term contains one subterm. This
94 > subterm cannot be extracted directly, as it may contain bound
95 > variables, which the user cannot work with directly.
96
97 ### `resolve(t: term, u: term): term`
98
99 Given a term _t_ and a term _u_, return either _t_ (if _t_ is
100 not an abstraction term) or _t_', where _t_' is a version of
101 _t_ where all bound variables in _t_' that were bound to _t_
102 itself have been replaced by _u_.
100103
101104 > **Note**: as stated above, a bound variable is always bound
102105 > to an abstraction term. The bound variables that are
103106 > replaced by a `resolve` operation are always those that are
104 > bound to _t1_.
107 > bound to _t_.
105108
106109 > **Note**: this operation was specifically not named `subst`,
107110 > as `subst` is often described as replacing *free* variables,
108 > while this replaces bound ones. It was also specifically not
109 > named `beta` or similar because it does not require _t1_ and _t2_
110 > to come from the same application term.
111 > while this operation replaces *bound* ones. It was also
112 > specifically not named `beta` because it does not require
113 > that _t_ and _u_ come from the same application term.
111114
112115 ### `destruct(t: term, f1: fun, f2: fun, f3: fun): X`
113116
119122 If _t_ is a free variable, evaluate _f1_(_n_) where _n_ is the name
120123 of the free variable _t_.
121124
122 If _t_ is an application term, evaluate _f2_(t1, t2) where _t1_ is
123 the head of _t_ and _t2_ is the tail of _t_.
125 If _t_ is an application term, evaluate _f2_(_u_, _v_) where _u_ is
126 the first subterm of _t_ and _v_ is the second subterm of _t_.
124127
125128 If _t_ is an abstraction term, evaluate _f3_(_t_).
126129
127130 > **Note**: the `destruct` operation's signature shown above was abbreviated to make
128131 > it look less intimidating. The full signature would be something more like
129132 >
130 > destruct(t: term, f1: fun(n: name): X, f2: fun(t1: term, t2: term): X, f3: fun(t: term): X): X
133 > destruct(t: term, f1: fun(n: name): X, f2: fun(u: term, v: term): X, f3: fun(t: term): X): X
131134 >
132
133 > **Note**: `destruct` is a "destructorizer" in the sense described
134 > in the [Destructorizers][] article. It is a slight variation on
135 > the conventional destructorizer pattern, but it is undoubtedly
136 > in the spirit of the thing.
137135
138136 > **Note**: while _f1_ and _f2_ "take apart" the term they are working
139137 > on, _f3_ does not, because the only operation that is allowed to
147145 These free variables may be located at any depth inside _t_, including
148146 inside any and all abstraction terms contained in _t_.
149147
150 > **Note**: I wish this operation was not required, but it seems it is
151 > needed in order to do many practical things with `destruct`. One
152 > would hope the list of free variables could be obtained by usage of
153 > `destruct` inside a recursive function, at it is simply a tree walk
154 > of the term. But the only practical way to "take apart" an abstraction
155 > term is to `resolve` it will a known free variable. But how do you
156 > pick that free variable, so that it will not collide with any of the
157 > free variables inside the term you are "taking apart"? Short of
158 > devising some clever namespacing for names, we need to know what
159 > free variables are insie the term first, _before_ `resolve`-ing it.
160 > Thus `freevars` exists to fulfil that purpose.)
161
162148 Stepping Back
163149 -------------
164150
170156 the next section), but one is not restricted to that. The lambda terms can be
171157 used for any purpose for which terms with name binding might prove useful.
172158
173 It is `destruct` that allows us to examine a lambda term.
159 It is `destruct` that allows us to examine a lambda term. `destruct` is a
160 "destructorizer" in the sense described in the [Destructorizers][] article.
161 It is a slight variation on the conventional destructorizer pattern, as it
162 does not "take apart" abstraction terms, but it is undoubtedly in the spirit
163 of the thing.
164
165 It is regrettable that `freevars` is an intrinsic operation rather than
166 something that can be built as a recursive function that usese `destruct`,
167 but it seems it is needed in order to use `destruct` with generality,
168 for the following reasons. The only practical way to "take apart" an abstraction
169 term is to `resolve` it with a known free variable. But how do you
170 pick that free variable, so that it will not collide with any of the
171 free variables inside the term you are "taking apart"? Short of
172 devising some clever namespacing for names, we need to know what
173 free variables are insie the term first, _before_ `resolve`-ing it.
174 Thus `freevars` exists to fulfil that purpose.
174175
175176 Some Examples
176177 -------------
178
179 ### Example 1
177180
178181 As a warm-up, suppose we want to write a function that tells us if a
179182 lambda term contains any free variable named `j`.
193196 let contains_j = fun(t, ns) ->
194197 destruct(r,
195198 fun(n) -> n == "j",
196 fun(t1, t2) -> contains_j(t1) || contains_j(t2),
199 fun(t, u) -> contains_j(t) || contains_j(u),
197200 fun(t) ->
198201 let
199202 (n, ns') = pick(ns, ~{"j"})
202205 contains_j(t')
203206 )
204207
205 Next: What if we want to get the set of free variables present
208 ### Example 2
209
210 What if we want to get the set of free variables present
206211 in a lambda term? We ought to be able to do this, and yet,
207212 it's difficult unless we know of a name that we are certain
208213 will not be among the names used by the free variables.
211216
212217 So for that task, we have `freevars` as one of the intrinsic
213218 operations.
219
220 TODO: instead have an example of using `freevars` and
221 passing it to `pick` and walking down arbitrary abstraction
222 terms this way.
223
224 ### Example 3
214225
215226 The next task is to write a beta-reducer. We destruct
216227 the term twice, once to ensure it is an application term,
230241 fun(t) -> t
231242 )
232243
244 ### Example 4
245
233246 The next task would be to search through a lambda term,
234 looking for a candidate application term to beta-reduce.
235 This doesn't sound hard. But is still not yet written
236
237 Discussion
238 ----------
239
240 There is nothing preventing an abstract data type which is a
241 proper superclass of this abstract data type, adding more operations.
242 However, many operations one might like to perform on these lambda
243 terms (such as reducing lambda terms to normal form, for instance)
244 ought to be expressible using `destruct`, possibly recursively.
247 looking for a candidate application term to reduce, and
248 reducing it.
249
250 --
251 -- Returns [bool, term] where bool indicates "has rewritten"
252 --
253 let reduce = fun(t) ->
254 if beta_reducible(t) then
255 [true, beta(t)]
256 else
257 destruct(r,
258 fun(n) -> [false, var(n)],
259 fun(t, u) ->
260 let
261 r = reduce(t)
262 in
263 if r[0] then
264 [true, app(r[1], u)]
265 else
266 let
267 s = reduce(u)
268 in
269 [s[0], t, s[1]],
270 fun(t) -> [false, t]
271 )
272
273 From there it ought to be just a hop, a skip, and a jump
274 to a proper lambda term normalizer.
245275
246276 [Destructorizers]: http://github.com/catseye/Destructorizers