lambda: Construction Diary & Job Jar
c000000>
2024-12-25 -09:55 -0800
|
|
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-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. | ||
| in progress 2024-06-22 |
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-12-25 I think the current approach to oLambda accounts for this and the use of oSigma(.ARG) as a check seems adequate. | |
| in progress 2024-12-25 |
2024-01-25 |
There is an accelerator, of course, for
|
|
| 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-12-25 When I tracked this down and mentioned it to Conal, I realized the connection was about paths to things and this is reflected in the oSigma.txt procedure on rewriting. The connection is pretty weak even though I didn't think so at the time. When I get into forms/states and assignments (with-expressions), it may be interesting how that will work, since it is more-like editing a struct.) | ||
| in progress 2024-07-12 |
2024-01-25 | The cover should provide a sketch of the essential ideas: The abstracting of a function from an expression. | |
|
done 2024-10-27 |
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/. | |
| done | 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 |