git @ Cat's Eye Technologies Lariat / a4c6c9d
Rewrites to Discussion section. Break into subsections. Chris Pressey 2 years ago
1 changed file(s) with 41 addition(s) and 30 deletion(s). Raw diff Collapse all Expand all
+41
-30
README.md less more
307307 Discussion
308308 ----------
309309
310 ### Prior work: Paulson's exercise
311
310312 The idea of formulating an ADT for lambda terms is not a new one.
311 In Chapter 9 of "ML for the Working Programmer" (Paulson 1991), the author
313 In Chapter 9 of "ML for the Working Programmer" (1991), Larry Paulson
312314 develops an implementation of lambda terms in ML and notes
313315
314316 > Signature LAMBDA_NAMELESS is concrete, revealing all the internal
315 > details. [...] An abstract signature for the lambda-calculus would
316 > provide operations upon lambda-terms themselves, hiding their
317 > details. [...] An abstract signature for the λ-calculus would
318 > provide operations upon λ-terms themselves, hiding their
317319 > representation.
318320
319 So if the idea is well established, why do we see so few implementations
320 of it out there? I think it's simply because it doesn't have a lot of
321 So if the idea is an established one, why does one see so few instances
322 of it out in the wild? I think it's simply because it doesn't have a lot of
321323 practical value in the usual contexts in which lambda term manipulation
322324 code is written -- that is to say, research contexts, where industrial
323 software engineering methods take a back seat.
324
325 In the context of Lariat, it is an object of study in its own right.
326
327 Now, here's the part I cut out of the paragraph from Paulson's book
328 quoted above:
325 software engineering methods take a back seat. Especially in theorem
326 provers, where a concrete representation may be significantly easier to
327 mechanically reason about.
328
329 In the context of Lariat, the ADT is the object of study in its own right.
330
331 Now, here's the part I cut out of the above quoted paragraph:
329332
330333 > Many values of type _term_ are **improper**: they do not correspond to
331 > real lambda-terms because they contain unmatched bound variable indices.
334 > real λ-terms because they contain unmatched bound variable indices.
332335 > [...] _abstract_ returns improper terms and _subst_ expects them.
333336
334337 And at the end of the section, he poses Exercise 9.16:
335338
336 > Define a signature for the lambda-calculus that hides its
337 > internal representation.
338
339 Which is sort of what I've done with Lariat, except he continues with
340
341 > It should specify predicates to test whether a lambda-term is a variable,
339 > Define a signature for the λ-calculus that hides its internal representation.
340 > It should specify predicates to test whether a λ-term is a variable,
342341 > an abstraction, or an application, and specify functions for abstraction
343342 > and substitution.
344343
345 But as he said earlier, substitution expects improper terms; so he appears
344 But, as he said earlier, substitution expects improper terms; so he appears
346345 to be asking for an abstract representation of lambda terms that includes
347 improper lambda terms.
348
349 Maybe that's OK for the sake of an exercise in a textbook, but that strikes
350 me as a poor abstraction. If you have an abstract object that represents
351 instances of something, it's best if your abstract object can _only_ represent
352 _valid_ instances of that thing.
346 improper lambda terms. (Either that or, based on his earlier remark about an
347 "abstract signature for the λ-calculus", he intended the operations in this
348 exercise to be on the level of the lambda calculus, i.e. beta-reduction and
349 normalization? But that's not what he wrote, so I shall take him at his word.)
350
351 I would argue that such an ADT has a lot less value to the programmer
352 than an ADT in which only proper lambda terms can be represented.
353353
354354 (For more information on this philosophy, see "Parse, don't Validate";
355355 [LCF-style-ND](http://github.com/cpressey/LCF-style-ND) illustrates how
356356 it applies to theorem objects in an LCF-style theorem prover; and it
357357 applies here too.)
358358
359 So if we have an ADT for lambda terms it's best if the ADT can _only_ represent
360 _proper_ lambda terms.
361
362 It was considering this point that led to the formulation of the Lariat ADT.
359 Although it was not in direct response to this exercise (which I hadn't
360 seen for years until I came across it again), but it was in consideration
361 of this point -- how does one formulate an ADT that represents only
362 proper lambda terms? -- that led me to the formulation of the Lariat ADT.
363
364 ### The role of `destruct`
365
363366 `var`, `app`, and `abs` construct terms, while `destruct` takes them apart.
364367 Constructing terms is the easy part; it's taking them apart properly that's
365368 hard.
368371 [this article on Destructorizers](http://github.com/cpressey/Destructorizers).
369372 In fact, this use case of "taking apart" lambda terms was one
370373 of the major motivations for formulating the destructorizer
371 concept. This is what allows the ADT to be "total".
374 concept.
375
376 Although it was not consciously intended, `destruct` is also what permits
377 the ADT to be "total" in the sense that there are no operations that are
378 undefined.
379
380 ### Equality modulo renaming of bound variables
372381
373382 When working with lambda terms, one is often concerned with
374383 comparing two lambda terms for equality, modulo renaming of bound
384393 be implemented in the implementation of the ADT
385394 (to correctly implement `destruct`), so could be exposed to the
386395 user as well.
396
397 ### The possibility of an algebraic formulation
387398
388399 The ADT that has been described in this document has been described
389400 quite precisely (I hope) but not formally. A direction that this