Implement σ.s (sigma.s), λ.x (lambda.x), and ρ.f (rho.f for rec.f)

[orcmid]

NOTE: This discussion was used for thinking-out-loud around the introduction of applicative-procedure-abstraction via oFrugal. These reflections are now incorporated and addressed in the miser/lambda documentation topic. That should be consulted before any further comments on this discussion. -- dh:2024-07-17

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 resembles that accomplished with expressions involving combinators. The technique is fashioned after that in [Rosenbloom1950: pp.116-118].

oMiser scripts are not expressions in the Combinatorial Arithmetic structure ‹ca› although applicative interpretation is comparable by design. For oMiser there needs to be accommodation, in particular, of script occurrences of .c, .d, and .ev along with other primitives having operator significance, including enclosures.

Details of oMiser scripts and their applicative-programming interpretations are established in obaptheory. This discussion presumes understanding of the Universal Applicative Functions there and of the notation employed for expressing scripts in oFrugalese. The informal sketch may provide helpful context to the more-formal specifications.

The abstraction operations described here have no failure detections. By convention abstraction failures tend to simply have no effect, producing an unchanged operand. In other cases the desired result is simply not achieved, without any indication of an aberration. Verification and confirmation of intended usages are important, as for all usage of oFrugal.

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] and enclosures, 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))

Some flattening (application-reducing) simplifications are possible depending on the forms of p and q in the p::q case. This is nicely demonstrated in the implementation of σ.s.

2. Introducing σ.s (sigma.s) for structure/insertion abstraction

2.1 Basic idea

(σ.s M) determines an ob which when applied (that is, taken as the script of an operation) to an operand ob t delivers ob M with t substituted for every occurrence of s.

This derivation does not consider the applicative interpretation of M, only its ob structure.

There are a number of useful properties that can be used in confirmation of operation. It also provides a rather complicated but very systematic means for determining some characteristics of M. In Frugalese,

(σ.s M)  s = M            //  always

(σ.s M)  = ` M            // when there is no occurrence of s in M.
is-enclosure(σ.s M)

is-enclosure(σ(.arg) M)   // when M is evidently not an applicative script

is-enclosure(σ(.self) M)  //  when M is evidently not a recursive or stateful applicative script

subst(v, s) M = (σ.s M) v  // is handy for substituting v for s everywhere in M

An important condition on the implementation of (σ.s M) is that constituents (branches) that do not contain s shall be enclosures as high up in the construction as possible; no reconstruction of that branch is required when applying (σ.s M) to an operand. That's how `M is arrived at when there is no occurrence of s.

Some examples,

lambda.z (x y z)
  = lambda.z (x :: y :: z)
  = x :: y :: .arg

sigma.z (x y z)
  = sigma.z (x :: y :: z)
  = .c :: x
       :: .c :: y
             :: .arg

sigma.x (x y z)
   = sigma.x (x :: y :: z)
   = .c :: .arg
          :: `(y :: z)

sigma.w (x y z)
   = sigma.w (x :: y :: z)
   = `(x :: y :: z)

2.2 An Implementation

σ.s M = if M = s
        then .arg                               
        else if is-individual(M)
             then ` M
             else if is-enclosure(M)
                  then let R = σ.s .a M
                        in if is-enclosure(R)
                           then ` M
                           else .e :: R
                  else let R = σ.s .a M,
                           S = σ.s .b M
                        in if is-enclosure(R) ∧ is-enclosure(S)
                           then ` M
                           else .c :: R :: S

Hand-compiling of this important function to an oFrugal script oSigma is provided at
oSigma.txt, The companion oSubst for subst(v, s) is provided there as well.

3. Deriving λ.x (lambda.x) abstraction of ob applicative interpretation

A simple heuristic is employed for determination of λ.x.

λ.x P = if is-enclosure(σ(.arg) P)
        then subst(.arg, x) P                               
        else σ.x P;

If there are no occurrences of .arg in P, then P is estimated to be in the form of a plain pseudo-oFrugal expression that is not already abstracted as an applicative-operation procedure. In that case, all occurrences of x are simply replaced by .arg to express P as an oFrugal script taking its operand wherever x occurred in P.

When there are occurrences of .arg in P, it is estimated that P is already an applicative-operation script and the appropriate transformation is a script that constructs P with all its occurrences of x replaced by its operand. In this case, it is usually required that x occur in an enclosure, since it is not to be evaluated immediately in such occurrences.

In either case, there may be further abstractions performed to achieve the intended complete applicative-operation script.

4. Deriving ρ.f (rho.f or rec.f) of applicative-interpretations of obs.

The derivation is now incorporated in the file lambda/oLambda.txt along with a comprehensive treatment of the lambda.x cases.

?. 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.

This is now addressed in the implementation, along with the heavy re-use of oSigma.

[Rosenbloom1950]

Rosenbloom, Paul. The Elements of Mathematical Logic. Dover Publications (New York: 1950). 2005 edition ISBN 0-486-44617-4 pbk.