// oLambda.txt 0.4.1                UTF-8                          2024-07-02
//--|----1----|----2----|----3----|----4----|----5----|----6----|----7----|--*
//
//                       OBAP ABSTRACTION FUNCTIONS
//                       ===========================
//
//          <https://orcmid.github.io/miser/lambda/oLambda.txt>
//
//           HAND-COMPILED λ.x and ρ.p ABSTRACTION OPERATIONS
//           ------------------------------------------------
//
//
//       The abstraction operations are introduced in Miser Project Discussion
//       Note #42, <https://github.com/orcmid/miser/discussions/42>.  This
//       oLambda.txt file provides for the manual compilation of the
//       λ.x and ρ.p Frugalese definitions into raw oFrugal ^oLambda and
//       oRec implementations.
//
//       The applicative computational scheme is defined in the file
//       <https://orcmid.github.io/miser/obap/obaptheory.txt>.
//
//       A sketch of oFrugal notation is at
//       <https://orcmid.github.io/miser/oFrugal/sketch.txt>.
//
//       The formal syntax and semantics of oFrugal expressions is at
//       <https://orcmid.github.io/miser/oFrugal/ob-exp.txt>.
//
//       Implementations of σ.s, subst(L, s), and δ.s(P) are relied upon.
//       Their definitions illustrate derivation of applicative-operation
//       scripts <https://orcmid.github.io/miser/lambda/oSigma.txt>.
//
//       See casep development for another demonstration of hand-compiling,
//       <https://orcmid.github.io/miser/oFrugal/casep.txt>.
//
//       This file is meant to be processable by oFrugal.
//
//
//               1. λ-Abstraction
//                  1.1 Heuristic
//                  1.2 Frugalese definition
//                  1.3 oFrugal derivation
//                  1.4 oFrugal definition
//               2. ρ-Abstraction
//               3. Least-Effort λ-Abstraction
//
//
//   1. λ-ABSTRACTION
//
//   1.1 Heuristic
//
//      The heuristic for λ-Abstraction via λ.x S has two rules:
//
//        1. If the ob S has no occurrences of .arg, the abstraction of
//           x from S is given by subst(.arg, x) S.
//
//        2. Otherwise, the abstraction of x from S is given by
//
//                      σ.x subst(` x, x) S.
//
//      These definitions depend on x being a lindy and not occuring in S
//      for any intended purpose other than treatment as an applicative-
//      expression "free-variable."
//
//
//    1.2 Frugalese Definition
//
//      λ.x S = if is-enclosure σ(.arg) S
//              then // no occurrence of .arg
//                   (subst(.arg) x) S
//              else σ.x subst(` x, x) S;
//
//      Note that σ(.arg) S yields enclosure ` S when there is no occurrence
//      of .arg in S.
//
//      When there is an occurrence of .arg in S, the operation is based on
//      the premise that for (λ.x S) P, the value of P is to be inserted into
//      S for use, without further use until applied-to or used-as an
//      operand in a subsequent application of ((λ.x S) P).
//
//      For a clear demonstration, it is valuable to conduct small tests,
//      such as interpretations of combinators and simple list-processing
//      operations.
//
//    1.3 oFrugal Derivation
//
//      λ =  λx λS //    if is-enclosure σ(.arg) S
//          .ev :: (is-enclosure :: ( σ :: `.arg ) :: S )
//
//              :: `( // then subst(.arg, x) S
//                       ((subst .arg) :: x) :: S
//                    ::
//                    // else σ.x subst(` x, x) S
//                       (σ :: x) :: ((subst :: ` x) :: x) :: S
//                    ) ;
//
//        = λx // λS    if is-enclosure σ(.arg) S
//          .ev :: (is-enclosure :: ( σ .arg ) :: .arg )
//
//              :: `( // then subst(.arg, x) S
//                       (((subst .arg) :: x) :: .arg)
//                    ::
//                    // else σ.x subst(` x, x) S
//                       (σ :: x) :: ((subst :: ` x) :: x) :: .arg
//                    ) ;
//
//        = ^δ(      sigarg, ` ^oSigma(.arg) )
//          ^δ(      subarg, ` ^oSubst(.arg) )
//
//          // λx λS        if is-enclosure σ(.arg) S
//
//          ^σ.x subst(` x, x)
//
//          `( .ev :: (is-enclosure :: sigarg :: .arg )
//
//                 :: `( // then subst(.arg, x) S
//                          ((subarg :: x) :: .arg)
//                       ::
//                       // else σ.x subst(` x, x) S
//                          (σ :: x) :: ((subst :: ` x) :: x) :: .arg
//                    )
//              );
//
//      bootstrapping λx in the definition by hand-following the Frugalse
//      definition.  We don't have to go farther because all of the functions
//      signified in the derivation are available.
//
//      Note that σ(.arg) and subst(.arg) are constant terms precomputed into
//      the script via ^δ(sigarg) and ^δ(subarg), an idiomatic practice
//      for introducing already-evaluated or -bound materials.
//
//    1.4 oFrugal Definition

!include "oSigma.txt"

!def ob ^oLambda
        = ^δ(is-enclosure, ` ^oIsEnclosure)
          ^δ(       subst, ` ^oSubst)
          ^δ(           σ, ` ^oSigma)
          ^δ(      sigarg, ` ^oSigma(.arg) )
          ^δ(      subarg, ` ^oSubst(.arg) )

          // λx λS        if is-enclosure σ(.arg) S

          ^σ.x subst(` x, x)

          `( .ev :: (is-enclosure :: sigarg :: .arg )

                 :: `( // then subst(.arg, x) S
                          ((subarg :: x) :: .arg)
                       ::
                       // else σ.x subst(` x, x) S
                          (σ :: x) :: ((subst :: ` x) :: x) :: .arg
                    )
              );
//
//   2. ρ-ABSTRACTION
//
//      The heuristic for ρ-abstraction is rather trivial.  It is based
//      on the assumption that it happens at the same time as the application
//      to the last operand, the one abstracted first.  Instead of inserting
//      .arg as in λ-abstraction, there is always a simple introduction of
//      .self along with the first abstracted operand.
//
//      ρp S = subst(.self, p) S
//
//      ρ = λp λS
//          subst(.self, p) S
//
//        = λp // λS
//          subst(.self) p
//
//        = // λp λS
//          subst .self;

!def ob ^oRec
        = ^oSubst(.self);


//   3. LEAST-EFFORT λ-ABSTRACTION
//
//   3.1 The Challenge
//
//      A limitation of ^oLambda (section 1) is the substantial work that
//      is performed by the overall
//
//          ^σ.x subst(` x, x)
//
//      When there will be only one of the two case depending on operand S.
//      It is worth looking at having two cases for operand x depending on
//      the condition satisfied by S.
//
//    3.2 Analysis
//
//      Consider,
//
//      λ.x S = ( if is-enclosure σ(.arg) S
//                then // no occurrence of .arg
//                     λ.x λ.S ((subst(.arg) x) S)
//                else λ.x λ.S (σ.x subst(` x, x) S)
//                )
//              (x, S);
//
//      with initial simplification,
//
//      λ.x S = ( if is-enclosure σ(.arg) S
//                then // no occurrence of .arg
//                     subst(.arg)
//                else λ.x λ.S (σ.x subst(` x, x) S)
//                )
//              (x, S);
//
//      Each arm of the conditional can be completely pre-computed, the point
//      of this alternative formulation.
//
//      I wanted to speak of this as "lazy" because the handling of operand x
//      is the least required depending on the nature of operand S.  And each
//      branch delivers a fixed precomputed value.  Because laziness is used
//      in another manner in contrast to the eager evaluation computational
//      model for oMiser, perhaps "opportunistic" or "minimalist" might be
//      preferable notions.  I chose "least-effort" as the feature of this
//      solution.
//
//       Since we already have an implementation of ^oLambda, We can make use
//       of it in bootstrapping to what should be a more-efficient version.
//
//    3.3 oFrugal Derivation
//
//      λ = λx λS //    if is-enclosure σ(.arg) S
//          ( ( (is-enclosure :: ( σ :: `.arg ) :: S )
//              ::
//              `( // then subst(.arg)
//                    (subst .arg)
//                 ::
//                 // else λ.x λ.S (σ.x subst(` x, x) S)
//                    (λ.x λ.S `(    (σ :: x)
//                                :: (subst :: .e :: x) :: x)
//                                :: S )
//                 )
//            :: x
//            )
//          :: S
//          );
//
//    3.4 oLambda Improvement

!def ob ^oLambda

        = ^δ( is-enclosure, ` ^oIsEnclosure)
          ^δ(       sigarg, ` ^oSigma .arg)
          ^δ(        subst, ` ^oSubst)
          ^δ(            σ, ` ^oSigma)

          ^δ(       subarg, ^oSubst .arg)
          ^δ(applicative-S, ^oLambda.x (    (σ :: x)
                                         :: ( (subst :: .e :: x) :: x )
                                         :: .arg )  )

          ^oLambda.x ^oLambda.S
              //    if is-enclosure σ(.arg) S
          `(  ( (is-enclosure :: sigarg :: S )
                ::
                `( // then subst(.arg)
                      subarg
                   ::
                   // else λ.x λ.S (σ.x subst(` x, x) S)
                      applicative-S
                  )
              :: x
              )
           :: S
           );

// Although it appears to be much work, effort is all on behalf of deriving
// the least-effort script.  Using the derived script is straightforward.
// We are putting oFrugal and the previous oLambda  to work.
//
// The sequences of ^δ introductions at the top of the definition is
// important.  Keep in mind the order in which these operations are all
// applied.  Also, notice that there is no need for .ev on the conditional
// results; they are already-computed.  This accounts for the differences in
// the ^δ-substitution of subarg and application-S from the others.
//
//--|----1----|----2----|----3----|----4----|----5----|----6----|----7----|--*
//
//                   Copyright 2024 Dennis E. Hamilton
//
//  Licensed under the Apache License, Version 2.0 (the "License");
//  you may not use this file except in compliance with the License.
//  You may obtain a copy of the License at
//              http://www.apache.org/licenses/LICENSE-2.0
//
//  Unless required by applicable law or agreed to in writing, software
//  distributed under the License is distributed on an "AS IS" BASIS,
//  WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
//  See the License for the specific language governing permissions and
//  limitations under the License.
//
//--|----1----|----2----|----3----|----4----|----5----|----6----|----7----|--*
//
// ATTRIBUTION
//
//   Hamilton, Dennis E. Hand-compiled λ.x and ρ.p Abstraction Operations.
//   Miser Theory Conception text file oLambda.txt version 0.4.1 dated
//   2024-07-02, available on the Internet as a version of
//   <https://orcmid.github.io/miser/lambda/oLambda.txt>
//
//--|----1----|----2----|----3----|----4----|----5----|----6----|----7----|--*
//
// TODO
//
// * Replace the Greek letters in early use of oFrugal.  Then revert to
//   that symbolism when oFrugal processes UTF-8.
//
//--|----1----|----2----|----3----|----4----|----5----|----6----|----7----|--*
//
// 0.4.1  2024-07-02T16:54Z Touch-ups, additional explanation
// 0.4.0  2024-06-24T15:46Z Use revised ^δ and explain better
// 0.3.0  2024-06-23T20:12Z Complete the Least-Effort λ-abstraction and use
//        oLambda to do it.
// 0.2.1  2024-06-22T19:23Z Initiate Least-Effort λ-abstraction treatment
// 0.2.0  2024-06-22T05:00Z Use ^δ for external definitions and
//        precomputations
// 0.1.0  2024-06-21T22:31Z Complete with definition of ρ-Abstraction and also
//        factor in pre-computation of some constant expressions.
// 0.0.2  2024-06-21T17:02Z Correct λ and oLambda derivations
// 0.0.1  2024-06-20T23:37Z First draft of Section 1, λ-Abstraction
// 0.0.0  2024-06-20T17:20Z Initial boilerplatwe from 0.3.2 oSigma.txt
//
//                         *** end of oLambda.txt ***