diff --git a/docs/oFrugal/casep.txt b/docs/oFrugal/casep.txt index 768fe42..00f68c6 100644 --- a/docs/oFrugal/casep.txt +++ b/docs/oFrugal/casep.txt @@ -1,4 +1,4 @@ -// casep.txt 1.3.0 UTF-8 2024-05-12 +// casep.txt 1.4.0 UTF-8 2024-06-08 //--|----1----|----2----|----3----|----4----|----5----|----6----|----7----|--* // // OBAP ABSTRACTION FUNCTIONS @@ -51,7 +51,7 @@ // In Frugalese pseudo-notation, this can be reformed into a form in // which the lambda-abstractions are explicitly applied. // -// casep = λ.v ρ.casepv λ.L (a) +// casep = λ.v ρ.casepv λ.L // (1) // ( if is-singleton(L) // then L // else if (.b .a L) v @@ -99,17 +99,17 @@ // so the first condition-form in casep (1a) translates to the oFrugal // form // -// .ev :: (.d :: L :: .b :: L) (a) +// .ev :: (.d :: L :: .b :: L) // (4) // :: `( L // :: not-satisfied-part ) // // // 5. THE CURRENT CASE-CONDITION CHECKING PART // -// The not-satisfied-part of (a) is another conditional form in (1a), +// The not-satisfied-part of (4) is another conditional form of (1), // thus // -// .ev :: ((.b :: .a :: L) :: v) (a) +// .ev :: ((.b :: .a :: L) :: ` v) // (5) // :: `( (.a :: L) // :: casepv :: .b :: L) // @@ -117,17 +117,18 @@ // oFrugal form in which the only remaining lindies are those which are // to be abstracted away. // -// One way to keep track of everything is by introduction of comments -// and also making of some intermediate oFrugal definitions to avoid -// recopying of portions already figured out. +// Note that v is enclosed, ensuring that at the level where (5) is +// evaluated, the previously-substituted operand value for v is simply +// used at that point, not evaluated further. +// // // // 6. PUTTING IT ALL TOGETHER // -// casep = λ.v ρ.casepv λ.L (a) +// casep = λ.v ρ.casepv λ.L // (6a) // (.ev :: (.d :: L :: .b :: L) // :: `( L -// :: .ev :: ((.b :: .a :: L) :: v) +// :: .ev :: ((.b :: .a :: L) :: ` v) // :: `( (.a :: L) // :: casepv :: .b :: L) // ) @@ -142,27 +143,27 @@ // oFrugal. With availability of an operating oFrugal implementation, // a dependable confirmation can also be established. -!def ob ^casep +!def ob ^casep // (6b) = ^λ.v ^ρ.casepv ^λ.L - ( // if is-singleton(L) + ( // if is-singleton(L) .ev :: (.d :: L :: .b :: L) - :: `( // then L + :: `( // then L L + :: + // else if (.b .a L) v + .ev :: ((.b :: .a :: L) :: ` v) - // else if (.b .a L) v - :: .ev :: ((.b :: .a :: L) :: v) - - :: `( // then .a L - (.a :: L) - - // else casepv .b L - :: casepv :: .b :: L - ) - ) - ); + :: `( // then .a L + (.a :: L) + :: + // else casepv .b L + casepv :: .b :: L + ) + ) + ); // assuming already-defined ^λ and ^ρ. // @@ -178,31 +179,31 @@ // // When a script-form is not yet for an applicative function taking any // operands, the λ.L heuristic will simply rewrite that script so that -// every occurrence of L is replaced by the primitive .ARG. +// every occurrence of L is replaced by the primitive .arg. // // 7.1 Abstracting Operand L -!def ob ^casep +!def ob ^casep // (7.1) = ^λ.v ^ρ.casepv // ^λ.L - ( // if is-singleton(L) - .ev :: (.d :: .arg :: .b :: .arg) + ( // if is-singleton(L) + .ev :: (.d :: L :: .b :: .arg) - :: `( // then L + :: `( // then L .arg + :: + // else if (.b .a L) v + .ev :: ((.b :: .a :: .arg) :: ` v) - // else if (.b .a L) v - :: .ev :: ((.b :: .a :: .arg) :: v) - - :: `( // then .a L - (.a :: .arg) - - // else casepv .b L - :: casepv :: .b :: .arg - ) - ) - ); + :: `( // then .a L + (.a :: .arg) + :: + // else casepv .b L + casepv :: .b :: .arg + ) + ) + ); // // 7.2 Abstracting the Recursion // @@ -215,25 +216,26 @@ // !def ob ^casep - = ^λ.v // ^ρ.casepv ^λ.L + = ^λ.v // ^ρ.casepv ^λ.L // (7.2) - ( // if is-singleton(L) - .ev :: (.d :: .arg :: .b :: .arg) + ( // if is-singleton(L) + .ev :: (.d :: L :: .b :: .arg) :: `( // then L .arg + :: + // else if (.b .a L) v + .ev :: ((.b :: .a :: .arg) :: ` v) - // else if (.b .a L) v - :: .ev :: ((.b :: .a :: .arg) :: v) - - :: `( // then .a L + :: `( // then .a L (.a :: .arg) - - // else casepv .b L - :: .self :: .b :: .arg - ) + :: + // else casepv .b L + .self :: .b :: .arg + ) ) - ); + ); + // // 7.3 Abstracting Operand v // @@ -242,18 +244,11 @@ // all occurrences of v by .ARG is incorrect. // // The required behavior in this case is to create a script that when -// applied to an operand, V, yields the above script but with `V in -// place of v. The quotation is required because we don't want to -// evaluate V, we want simply to use it in the form that is supplied -// as an operand. -// -// Forms of the abstraction function, σ.v, are useful in this case. -// Here, we provide that function manually. We will, at this stage, -// have a loss of similarity with the Frugalese pseudo-language form -// that we started with. +// applied to an operand, V, yields the above script but with V in +// place of v. // // This version is obtained by manually applying the algorithm in -// sigma.txt . +// oSigma.txt . !def ob ^casep @@ -280,8 +275,7 @@ ); // demonstrating why it is important to have the abstraction functions -// up-and-running, with easier confirmation and, if necessary, saving -// definitions to a text file. +// up-and-running, with easier confirmation and simpler expresssion. // // //--|----1----|----2----|----3----|----4----|----5----|----6----|----7----|--* @@ -304,7 +298,7 @@ // ATTRIBUTION // // Hamilton, Dennis E. Hand-Compiled casep(v, L). Miser Theory -// Conception text file casep.txt version 1.3.0 dated 2024-05-12, +// Conception text file casep.txt version 1.4.0 dated 2024-06-08, // available on the Internet as a version of // // @@ -314,10 +308,10 @@ // // * Test this with oFrugal when implementation is available. // -// * Continue making this more-readable following section 4. // //--|----1----|----2----|----3----|----4----|----5----|----6----|----7----|--* // +// 1.4.0 2024-06-98T16:06Z More clarifications, better layout, tying in oSigma // 1.3.0 2024-05-12T20:41Z Cleanit it all up // 1.2.4 2024-05-11T21:36Z Completed polishing ^casep for now. // 1.2.3 2024-05-11T16:46Z Use intermediates to make conditionals more