lambda: Construction Diary & Job Jar
c000000>
2024-08-22 -11:48 -0700
|
|
lambda: Construction Diary & Job Jar |
|
Status |
Date |
Description |
|
| 2024-08-22 | I need to rationalize the use of the λx and similar notations around here, when applying it to Frugalese. One might be by using bold. And always using the d-forms in the typical cases. I need an example that indicates how λ.x and λ(x) and λ.(x) are, applicatively, all the same, so long as x is a term. This needs to be tidied up. | ||
| 2024-08-22 | I am giving up on trace and "maeby" in favor of symbolic forms. The obaptheory.txt must be updated to reflect that. And we will speak of it properly in other parts of the project, including here on lambda/. | ||
| 2024-08-12 | I need to understand about the Curry-Howard correspondence and Cartesian Closed Category as it shows up there. I then need to reconcile that with [Feferman1977]. | ||
| 2024-02-05 | We will need to test that ^lambda does work as λ when given applicative forms of combinators. It will be important to see how close we can get to the hand-built combinator interpretations in combinators.txt | ||
| 2024-02-05 | I need to make clear that ^lambda is not the lambda of combinatory logic, although it is the same idea, that of abstracting out a literal/variable to make a script that accepts an operand in that place. Part of it has to do with the presence of primitives that influence the applicative structure of a script. These all factor into the arrangement. It also means there can be weird cases not accounted for in the interpretation of combinators in ‹obap›. Fortunately, the introduction of extension by establishment of individuals in ‹obapx› allows us to be somewhat extension-indifferent in the definition of ^lambda and ^rec. | ||
| 2024-01-25 | I am wondering if there is an accelerator for whether or not an ob, taken as a procedure script, has an exposed evref, i.e., has-evref(p). I might have to separate the two cases. But this would influence how parsing of p happens in working out where and how to restructure. I need to work out the structure first to deal with this and find good cases. | ||
| 2024-01-25 | There is an accelerator, of course, for is-pure-lindy-trace and it can be handled by a flag bit in the storage structure for an ob element. Whether it is set or not on ob.NIL is something to be worked out. It seems safe to do so. It is easy to then set the flag bit on the result of an ob.c(x, y) operation. | ||
| 2024-01-25 | The rewriting that happens in abstracting lambdas from combinators or from oMiser procedures is very similar to a list-structure editing mechanism that I saw Conal Elliott (http://conal.net/) describe in a blog post somewhere. I will mention that, although the particular procedure for lambda abstraction is similar in terms of how the rewriting works although it is not established in the same way. | ||
| 2024-01-25 | The cover should provide a sketch of the essential ideas: The abstracting of a function from an expression. | ||
| 2024-01-25 | Provide a hybrid stub page for lambda/ | ||
| done | 2024-01-25 | Introduce a clean construction zone | |
| done | 2024-01-25 |
|
|
 |
You are navigating
construction material of the Miser Project |
created 2024-01-08T19:12Z by orcmid |