Commit 0b4b96eb89fabb84b3c9e560ae484b8314cf477c - Lariat

Edits to README. Chris Pressey 3 years ago

1 changed file(s) with 22 addition(s) and 38 deletion(s). Raw diff Collapse all Expand all

+22

-38

README.md less more

76	76	### `equal(n: name, m: name): boolean`
77	77
78	78	Given a name _n_ and a name _m_, return true if they are identical names,
79		or return false otherwise.
	79	otherwise return false.
80	80
81	81	### `fresh(ns: set of name): name`
82	82

88	88	discussion on implementation, see [Appendix A](#appendix-a).
89	89
90	90	The operation should be deterministic in the sense that, given the
91		same set, it should return the same name.
	91	same set of names, it should always return the same fresh name.
92	92
93	93	> Note: It is not required that the `fresh` operation be
94	94	> exposed to the user; it is, rather, a structural requirement

104	104	The Operations
105	105	--------------
106	106
107		_YET TO BE FINALIZED_
108
109	107	### `var(n: name): term`
110	108
111	109	Given a name _n_, return a _free variable_ with the name _n_.
112	110
113	111	> Note: A free variable is a term; it can be passed to any operation
114	112	> that expects a term.
115
116		> Note: A name is a qualified name, described in the section "Names"
117		> above this one.
118	113
119	114	### `app(t: term, u: term): term`
120	115

186	181
187	182	### Example 1
188	183
189		As a warm-up, suppose we want to write a function that tells us if a
190		lambda term contains any free variable named (for the sake of
191		concreteness, let's say) `j`.
192
193		In this implementation and those that follow, we will assume we have
194		a simple functional language with the usual accoutrements (recursion,
195		`if`, `let` and so forth).
196
197		We also rely on the fact that, when we `destruct` an abstraction
198		term, the fresh variable it will pick, will not be `j`. This is true
199		whether or not `j` is one of the free variables in the abstraction
200		term being destructed, because according to the algorithm, a fresh
201		variable's qualified name will always have more than one name segment.
202
203		let contains_j = fun(t) ->
204		destruct(t,
205		fun(n) -> n == "j",
206		fun(u, v) -> contains_j(u) \|\| contains_j(v),
207		fun(u, n) -> contains_j(u)
208		)
209
210		### Example 2
211
212	184	A common task is to obtain the set of free variables present
213	185	in a lambda term. This is not difficult; we only need to
214	186	keep track of the new free variables we introduce ourselves
215		when we `destruct` an abstraction term.
	187	when we `destruct` an abstraction term, and make sure not to
	188	include any of them when we report the free variables we found.
216	189
217	190	let freevars = fun(t, ours) ->
218	191	destruct(t,

221	194	fun(u, n) -> freevars(u, ours + {n})
222	195	)
223	196
224		### Example 3
	197	### Example 2
225	198
226	199	Given an abstraction term and a value, return a version of
227	200	the body of the abstraction term where every instance of the

248	221	because it does not require that _t_ and _x_ come from the same
249	222	application term.
250	223
251		### Example 4
	224	### Example 3
252	225
253	226	The next task is to write a beta-reducer. We destruct
254	227	the term twice, once to ensure it is an application term,

273	246	implementation of `resolve` and this would save a call
274	247	to `destruct`.
275	248
276		### Example 5
	249	### Example 4
277	250
278	251	The next task would be to search through a lambda term,
279	252	looking for a candidate application term to reduce, and

320	293	Discussion
321	294	----------
322	295
323		_YET TO BE FINALIZED_
324
325	296	`var`, `app`, and `abs` construct terms, while `destruct` takes them apart.
326	297	Constructing terms is the easy part; it's taking them apart properly that's
327	298	hard.
328	299
329	300	`destruct` is a "destructorizer" in the sense described in
330	301	[this article on Destructorizers](http://github.com/cpressey/Destructorizers).
	302	In fact, this use case of "taking apart" lambda terms was one
	303	of the major motivations for formulating the destructorizer
	304	concept.
331	305
332	306	When working with lambda terms, one is often concerned with
333	307	comparing two lambda terms for equality, modulo renaming of bound

336	310	render the two terms as text (or some other concrete representation),
337	311	then compare the texts for equality.
338	312
	313	But of course such an operation could be provided as a native
	314	operation for performance or convenience. Similarly, although
	315	we have shown that we can implement `freevars` using the operations
	316	of the abstract data type, it is expected that it would already
	317	be implemented in the implementation of the abstract data type
	318	(to correctly implement `destruct`), so could be exposed to the
	319	user as well.
	320
339	321	Appendices
340	322	----------
341	323
342	324	### Appendix A
343	325
344	326	#### On the implementation of names.
345
346		_TO BE REWRITTEN_
347	327
348	328	One way to implement names as defined in Lariat 0.2 is to use _qualified names_.
349	329	A qualified name is an ordered list of _name segments_, where each name segment

366	346
367	347	In addition, a simple way to pick an arbitrary name segment to prepend to
368	348	it, is to look at the leftmost name segment already in the qualified name.
	349
	350	So we can assume an algorithm like this is in use. But ultimately, any
	351	implementation which satisfies the two operations required of names
	352	(`equal` and `fresh`) is acceptable.