git @ Cat's Eye Technologies Lariat / b0d76ef
Many edits, especially to discussion. Add footnotes section. Chris Pressey 2 years ago
1 changed file(s) with 106 addition(s) and 77 deletion(s). Raw diff Collapse all Expand all
+106
-77
README.md less more
6363 from the programmer) so long as the implementation of the operations conforms
6464 to the stated specification.
6565
66 This ADT is designed for simplicity rather than performance. It is a minimal
66 This ADT is designed for simplicity and elegance rather than performance. It is a minimal
6767 formulation that does not necessarily make any of commonly-used manipulations
6868 of lambda terms efficient.
6969
70 This ADT has two properties.
71
70 This ADT has two properties, intended to contribute to its elegance.
7271 Firstly, it can represent only _proper_ lambda terms; that is, it is not possible
7372 for a lambda term constructed by the Lariat operations to contain an invalid
7473 bound variable.
7675 Secondly, it is _total_ in the sense that all operations are defined
7776 for all inputs that conform to their type signatures. There are no conditions
7877 (such as trying to pop from an empty stack in a stack ADT) where the result is
79 undefined, or defined to return an error condition. This totality does, however,
78 undefined, nor any defined to return an error condition. This totality does, however,
8079 come at the cost of the operations being higher-order and with polymorphic types.
8180
8281 For more background information, see the [Discussion](#discussion) section below.
8483 Names
8584 -----
8685
87 In any explication of name binding we must deal with names. As of 0.3, Lariat
88 requires only two properties of names.
86 Lambda terms are essentially about name binding, and in any explication of name binding,
87 we must deal with names. As of 0.3, Lariat requires only two properties of names.
8988
9089 Firstly, it must be possible to compare two names for equality. This is
91 required for operations that replace a free variable with a given name
90 required for operations that replace free variables that have a given name
9291 with a value -- there must be some way for them to check that the free
9392 variable has the name that they are seeking.
9493
9594 Secondly, given a set of names, it must be possible to generate a new name that
96 is not equal to any of the names in the set (a so-called "fresh" name).
97 This facility is not directly exposed as an operation, but is required
98 to properly implement the `destruct` operation. Obtaining a fresh name could
99 be as simple as modelling names as natural numbers, taking the maximum of a
100 set of names (natural numbers) and adding 1 to it.
95 is not equal to any of the names in the set (a so-called "fresh" name). This is
96 required to properly implement the `destruct` operation. If names are modelled
97 as character strings, obtaining a fresh name could be as simple as finding the
98 longest string of a set of strings, and prepending `"a"` to it.
10199
102100 Note that, although neither of these properties is exposed as an operation,
103 it would be reasonable for a practical implementation of Lariat to do so.
104
105 And beyond these basic properties, it would also be reasonable to provide
101 it would be reasonable for a practical implementation of Lariat to expose
102 them so. It would also be reasonable to provide
106103 other operations on names, such as constructing a new name from a textual
107104 representation, rendering a given name to a canonical textual representation,
108105 and so forth. From the perspective of Lariat itself these are ancillary
173170 > bound to the abstraction term being `destruct`ed.
174171
175172 > **Note**: the `destruct` operation's signature shown above was abbreviated to make
176 > it look less intimidating. The full signature would be
173 > it less intimidating. The full signature would be
177174 >
178175 > destruct(t: term, f1: fun(n: name): X, f2: fun(u: term, v: term): X, f3: fun(u: term, n: name): X): X
179176 >
325322 > representation.
326323
327324 So the idea is an established one; but if so, why does one see so few instances
328 of it out in the wild? I think it's simply because it doesn't have a lot of
329 practical value in the usual contexts in which lambda term manipulation
330 code is written -- that is to say, research contexts, where industrial
331 software engineering methods take a back seat. Especially in theorem
332 provers, where a concrete representation may be significantly easier to
333 mechanically reason about.
334
335 In the context of Lariat, the ADT is the object of study in its own right.
336
337 Now, here's the part I cut out of the above quoted paragraph:
325 of it out in the wild? I think it's this: most lambda term manipulation code
326 sees actual use only academic contexts, most usually in such things as theorem provers.
327 These are contexts that don't greatly benefit from the software
328 engineering principle of being able to swap out one implementation
329 of an interface with an alternative implementation. Indeed, in a
330 theorem proving context, an extra level of abstraction may just
331 be another burden that the mechanical reasoning methods need to
332 deal with, with no other benefit. So concrete data types are used,
333 because concrete data types are sufficient.
334
335 In the context of Lariat, however, the ADT is the object of study in its own right.
336
337 Now, here's the part I elided from the above quoted paragraph:
338338
339339 > Many values of type _term_ are **improper**: they do not correspond to
340340 > real λ-terms because they contain unmatched bound variable indices.
349349
350350 However, as he mentioned earlier, these operations produce and expect improper
351351 terms; so he appears to be asking for an abstract representation of lambda terms
352 that includes improper lambda terms. (Either that or, based on his remark about
353 an "abstract signature for the λ-calculus", he intended the operations in this
354 exercise to be on the level of the lambda calculus, i.e. beta-reduction and
355 normalization? But that's not what he wrote, and lacking a copy of the 2nd
356 edition to see if this has been corrected, I shall take him at his word.)
357
358 I would argue that such an ADT has a lot less value to the programmer
352 that includes improper lambda terms. [[Footnote 1]](#footnote-1)
353 I would argue that such an ADT has a lot less value as an abstraction
359354 than an ADT in which only proper lambda terms can be represented.
360
361 (For more information on this philosophy, see "Parse, don't Validate";
362 [LCF-style-ND](http://github.com/cpressey/LCF-style-ND) illustrates how
363 it applies to theorem objects in an LCF-style theorem prover; and it
364 applies here too.)
355 [[Footnote 2]](#footnote-2)
365356
366357 Although it was not in direct response to this exercise (which I hadn't
367358 seen for years until I came across it again), it was consideration
380371 of the major motivations for formulating the destructorizer
381372 concept.
382373
383 Although it was not consciously intended, `destruct` is also what permits
374 Although it was not specifically intended, `destruct` is also what permits
384375 the ADT to be "total" in the sense that there are no operations that are
385376 undefined.
386377
391382 variables. We haven't introduced such an operation because it should
392383 be possible to build such an operation using `destruct`; basically,
393384 render the two terms as text (or some other concrete representation),
394 then compare the texts for equality.
395
396 (The procedure for obtaining a fresh name needs to be deterministic
397 for this to work properly, so that the fresh names generated when
398 `destruct`ing two equal abstractions, match up in both of the terms.)
399
400 But of course such an operation could be provided as a native
401 operation for performance or convenience. Similarly, although
402 we have shown that we can implement `freevars` using the operations
403 of the ADT, it is expected that it would already
404 be implemented in the implementation of the ADT
405 (to correctly implement `destruct`), so could be exposed to the
406 user as well.
385 then compare the texts for equality. (This does however require that
386 thete is an operation for rendering a name to its textual representation,
387 and also that the procedure for obtaining a fresh name is deterministic,
388 so that the fresh names generated when `destruct`ing two equal abstractions,
389 match up in both of the terms.)
390
391 Of course, such an operation could be provided as a native
392 operation for performance or convenience. (This is one of the nice
393 things about ADTs -- they can be sub-ADTs of a larger ADT.) Similarly,
394 although we have shown that we can implement `freevars` using the operations
395 of the ADT, the definition of the `destruct` operation essentially requires
396 that something equivalent to it already exists, and it could be exposed to
397 the user as well.
407398
408399 ### The possibility of an algebraic formulation
409400
416407 There are reasons to believe this is not impossible. In
417408 [The Lambda Calculus is Algebraic](https://www.mscs.dal.ca/~selinger/papers/combinatory.pdf) (PDF)
418409 (Selinger, 1996) an algebra equivalent to the lambda calculus is
419 formed by treating free variables as "indeterminates", although
420 I'm not entirely certain what is meant by that.
421
422 However, the use of `destruct` complicates this, as it is a "higher-order"
423 operation, in the sense that it takes functions as parameters. This would
424 likely make reducing it to a set of equations highly non-straightforward.
425
426 To go this route, it would be much more straightforward to refactor Lariat
427 into a "partial" ADT, one which does not have `destruct` but does have
428 a set of discrete operations such as `is_app`, `app_lhs`, `app_rhs`, and
429 so forth. This would be more like a conventional ADT, e.g. a stack
430 ADT which has `is_empty` and for which popping an empty stack is simply
431 undefined.
432
433 This "partial" ADT would still face some complications, though, when
434 it comes to deconstructing abstractions formed by `abs`; it could
435 pick a fresh variable for resolving the binding (and in fact would
436 need to, because the user would not be properly equipped to supply a
437 suitable one), but it would also need to return that variable, along
438 with the deconstructed contents, to the user, so that they could
439 sensibly detect what transformation was applied to the contents
440 to ensure that the contents did not contain improper bound variables.
441
442 Working the resulting equational theory out in detail is potential
443 future work here.
410 formed by treating free variables as "indeterminates" (although
411 I must admit I'm not entirely certain what is meant by that).
412 Additionally, section 1.3 of [Language Prototyping: An Algebraic Specification Approach](https://archive.org/details/languageprototyp0000unse)
413 (1996; van Deursen, Heering, Klint eds., borrowable online at archive.org)
414 gives a definition of the lambda calculus in the algebraic definition
415 language ASF+SDF, which comes fairly close to conventional equational logic
416 (although it does contain extras such as conditional equations).
417
418 However, in Lariat, `destruct` is a "higher-order" operation,
419 in the sense that it takes functions as parameters, and this may
420 well complicate the task of defining an equational theory based
421 on Lariat, or it may complicate the resulting equational theory.
422 We'll talk about that in the next section.
423
424 ### Variation: Partial Lariat
425
426 To support the effort of formulating an algebra based on Lariat,
427 or for any other purposes which it may suite, it's worth looking at the possibility
428 of replacing `destruct` with a set of "first-order" operations.
429
430 When I first started working out Lariat, I thought that using a
431 destructorizer would be essential to the problem of being able to
432 destruct an abstraction term and have the result be a proper lambda term.
433 It's not as essential as I thought. What `destruct` does when given
434 an abstraction term is, basically, to form a free variable with a
435 fresh name (one that does not occur in the abstraction term) and
436 `resolve` (as defined in the examples above) the abstraction term with it.
437 If the ADT were to have discrete operations for picking a fresh name
438 given a lambda term, and for `resolve`, these could be applied
439 "manually", and in this manner the user could destruct abstraction
440 terms just the same as `destruct` does.
441
442 There are subtle differences: `resolve` would need to be an intrinsic operation
443 which is exposed by the ADT, rather that derived from the basic operations
444 of Lariat. It also gives the user the freedom to apply `resolve` with whatever
445 they wish, while in Lariat, `destruct` can only apply this action with a fresh
446 variable that it itself has chosen, which is significantly more restrictive.
447
448 A version of Lariat without `destruct` would also need operations
449 for testing if a term is an abstraction term, vs. an application
450 term, vs. a free variable. The operation of extracting the first
451 and second values from an application term (basically, the theory
452 of ordered pairs) would not be sensibly defined for abstraction
453 terms or free variables, and so this version of the ADT would be
454 partial rather than total, thus the name "Partial Lariat".
455
456 Footnotes
457 ---------
458
459 #### Footnote 1
460
461 Either that or, based on his remark about
462 an "abstract signature for the λ-calculus", he intended the operations in this
463 exercise to be on the level of the lambda calculus, i.e. beta-reduction and
464 normalization? But that's not what he wrote, and lacking a copy of the 2nd
465 edition to see if this has been corrected, I shall take him at his word.
466
467 #### Footnote 2
468
469 For more information on this philosophy, see "Parse, don't Validate";
470 in particular, [LCF-style-ND](http://github.com/cpressey/LCF-style-ND)
471 illustrates how it applies to theorem objects in an LCF-style theorem prover;
472 and it applies here too.