One of the key features to be established for oMiser is the availability of heuristics by which ρλ-abstraction is performed on Obs taken to be scripts.
The basic approach is based on how that is accomplished with expressions involving combinators. The technique is fashioned after that in [Rosenbloom1950: pp.116-118].
oMiser scripts are not expressions in ‹ca› and there needs to be accommodation, in particular, of the occurrences of .C, .D, and .EV in particular, along with other primitives having operator significance, including enclosures.
It may be the case that operation of the mechanized procedures may depend on adherence to certain amenable forms of scripts. In that case, failure modes may need to be addressed as well.
1. The Basic Idea
Fundamentally, λ.x(e) in terms of combinators follows the following pattern when there are no special forms. In ‹ca›, we have
λ.x(e) = |Ke for e a term different from x
= I when e = x
λ.x(|pq) = ||S(λ.x(p))(λ.x(q))
In the absence of special forms (Obap6: speccialop or evref), there are direct counterparts in the ‹ob› computation model.
λ.x(e) = ^cK(e) = ` e, when e is a term not x
= ^cI = ob.NIL, when e = x
λ.x(p :: q) = ^cS(λ.x(p))(λ.x(q))
There is often an opportunity for in-lining, leading to the simplification
λ.x(e) = ` e, when e is a term not x
= .ARG , when e = x
λ.x(p :: q) = λ.x(p) :: λ.x(q)
when minding our p's and q's.
2. Engineering Considerations
Essentially, if x is not free in λ.x(e), we want λ.x(e) = _e_ or just _e_ when eval(_e_) = eval(e), e being literal in some sense.
When x occurs in λ.x(e), we want those occurrences replaced by .ARG in a script such that ap( λ.x(e), v) yields the same as eval(e) with `( v) everywhere that x was.
The λ.x(e) computation operates by recursive descent into the components of e. On the ascend back to assembly of the final script, steps are taken to minimize reconstruction. The more parts of e that can be retained as either literals or enclosures in λ.x(e) the better, including reaching the `(e) or literal e case.
[to be continued]
[Rosenbloom1950]
Rosenbloom, Paul. The Elements of Mathematical Logic. Dover Publications (New York: 1950). 2005 edition ISBN 0-486-44617-4 pbk.
One of the key features to be established for oMiser is the availability of heuristics by which ρλ-abstraction is performed on Obs taken to be scripts.
The basic approach is based on how that is accomplished with expressions involving combinators. The technique is fashioned after that in [Rosenbloom1950: pp.116-118].
oMiser scripts are not expressions in ‹ca› and there needs to be accommodation, in particular, of the occurrences of .C, .D, and .EV in particular, along with other primitives having operator significance, including enclosures.
It may be the case that operation of the mechanized procedures may depend on adherence to certain amenable forms of scripts. In that case, failure modes may need to be addressed as well.
1. The Basic Idea
Fundamentally, λ.x(e) in terms of combinators follows the following pattern when there are no special forms. In ‹ca›, we have
In the absence of special forms (Obap6: speccialop or evref), there are direct counterparts in the ‹ob› computation model.
There is often an opportunity for in-lining, leading to the simplification
when minding our p's and q's.
2. Engineering Considerations
Essentially, if x is not free in λ.x(e), we want λ.x(e) =
_e_ or just _e_ when eval(_e_) = eval(e), e being literal in some sense.When x occurs in λ.x(e), we want those occurrences replaced by .ARG in a script such that ap( λ.x(e), v) yields the same as eval(e) with `( v) everywhere that x was.
The λ.x(e) computation operates by recursive descent into the components of e. On the ascend back to assembly of the final script, steps are taken to minimize reconstruction. The more parts of e that can be retained as either literals or enclosures in λ.x(e) the better, including reaching the `(e) or literal e case.
[to be continued]