Monday, December 3, 2018

Miser Project: Representing Functions in ‹ob›’s Abstract World

2019-11-12 Editing: Repair reflow where formulas are mangled.  Other touch-ups.
2019-11-05 Update: Complete separation from the WordPress version.
2019-11-03 Update: Touch-ups with initial migration to Blogger

2019-01-02 Update: Corrects ob.p01.bp representation of x ⊆ y and simplifies ob.p01.bp.is-eq(x,y) in boole.txt section 2.5.
2018-12-12 Update: The Boolean Algebra ob.bvx representations are adjusted to employ short-circuits and the ob.bvx.bvn interpretation improved.  Some things I just can’t let go by.
2018-12-10 Update: Representation of Boolean Algebra ob.bvx is simplified to make interpretation of ‹bvn› more direct and properly extensible.
2018-12-07 Update: Revamp the development of ob.bvx for interpretation of all Boolean Algebra structures via inter-interpretation, exposing more about the connection of mathematical structures and computational ones while also exposing the differences.

The structure ‹ob› = 〈Ob,Of,Ot〉is a mathematical, logical-theory conception that has  computational interpretation.  Software implementation for such an interpretation has been demonstrated.   So far, this is just for a depiction of some distinguished individuals (ob.NIL and lindies) and all the constructions possible over those.  The distinction of additional individuals is open-ended.

There are also canonical forms for all of the distinguished obs. This has obs be definite, however mathematically abstract.  It also has obs be finitely-expressible, even though there is no bound on the domain, Ob.

Representation of data, where obs are taken as encodings of data, thereby being interpretations of some other conception, has been suggested as a prospect for ‹ob›.  Now we turn to representation of functions and then representation of some structures other than ‹ob› .  The interpretations involved are mathematical in nature, not computational however suggestive they might be.

The separation (and useful connection) between mathematical characterizations and computational ones becomes more clear when we consider reasoning about functions and their representations in effectively-computable form, first the Of in ‹ob› and then representations and interpretations of other structures among each other and in ‹ob›. 

Preliminaries

  1. Hark! Is That a Theory I See Before Me?
  2. ‹ob› Primitive Functions
  3. Narrowing ‹ob› for Computational Interpretation
  4. Representing Data as Obs

1. The Abstraction of Functions

In structure ‹ob› = 〈Ob,Of,Ot〉, the characterization of functions in Of is by introduction of definitions using the theory language, Ot, just as there are mathematical expressions of the primitive notions.   Characterization in this manner demonstrates that the primitive functions and many other functions are in Of.

The way that a function f( x1, x2, .., xn ) is successfully represented by an effectively-computable representation in Ot (or any other structure on the same principles as employed for ‹ob› here)  is with a small number of logical statements such that,

  • there is a finite number of statements of finite length in the characterization.
  • For definite operands, x1, x2, .., xn, the definitions pertaining to
             f( x1, x2, .., xn )
    lead to deduction, in a finite number of steps, to at most one definite result,
         y = f( x1, x2, .., xn ).
  • It can be the case that there is no definite result for some operands, xi.
    • When there is a definite result for all definite operands, x1, x2, .., xn, f is said to be a total function.  It is defined on all obs.
    • When there is no definite result for all definite operands,
      x1, x2, .., xn, f is said to be a partial function that is undefined for those operands.
    • It is not always possible to determine, from the offered characterization, whether a function is total or not.
Given two distinct representations in this manner, seemingly for function f and for function g,
  • If f( x1, x2, .., xn ) = g( x1, x2, .., xn ) is deducible for all definite x, where each have definite result, we say that the same function is represented.
  • We expect no counterpart of canonical forms for functions.  Determination that two representations are for the same function involves a mathematical proof.
  • Determination that two representations are not for the same function is often by directly exhibiting operands x1, x2, .., xn, for which
            f( x1, x2, .., xn ) ≠ g( x1, x2, .., xn )

The prospect of partial functions is unfortunate, with total functions much more easily dealt with.  Nevertheless, there will be cases where partial functions are convenient and important cases where they are unavoidable.

Establishment of identities is commonplace in algebra, trigonometry, introductory calculus, and other areas of early mathematical education and practice.  Identities serve to address practical questions, involve rather direct forms of proof, and can be used to find attractive computational interpretations.

These notions in the context of ‹ob› and the Miser Project become more familiar on exploration of examples.

1.1 The Blast Function

In our structure ‹ob› = 〈Ob,Of,Ot〉there is a function in Of that can be represented, using Ot, in the following fashion.
  • bLast1.  ob.is-singleton( x )  ⇒ bLast( x ) = x
  • bLast2. ¬ ob.is-singleton( x )  ⇒ bLast( x ) = bLast(ob.b( x ))
By reference to the definition of primitive notions given earlier, we can summarize
  • bLast( x ) is the singleton that is at the end of a chain of successive ob.b( x )
    compositions, ob.b( … (ob.b( x )) … ), keeping in mind that for any singleton,
          ob.b( x ) = x.
  • bLast( x ) is total -- defined for every possible definite ob, x.
  • The name “bLast” was chosen to signify the determination of the ob that is at the first ob.b that makes no difference, the last ob.b in the chain.

Let ob t1 = a1 :: (a2 :: b2) :: .NIL (using the CFob canonical form for ob t1)
where a1, a2, and b2 are lindies, distinct individuals.  Then

    bLast( t1 ) = bLast( ob.b( t1 ) )
                     = bLast( ob.b( (a2 :: b2) :: .NIL) )
                     = bLast(.NIL)
                     = .NIL,

and the equational progression is typical for streamlining the progression of deductions.  At each step, exactly one of bLast1 and bLast2 apply.

1.2 The Mirror Function 

  • Mirror1. ob.is-singleton( x )  ⇒ mirror( x ) = x
  • Mirror2. ¬ ob.is-singleton( x
         ⇒ mirror( x ) = ob.c(mirror(ob.b( x )), mirror(ob.a( x )) )
Here mirror( x ) is a form of mirror-image of the ob x.  Using ob t1 from above,


mirror( t1 )
         = ob.c(mirror((a2 :: b2) :: .NIL), mirror(a1)) )
         = ob.c(mirror(.NIL), mirror(a2 :: b2)) :: a1
         = (ob.c(.NIL, ob.c(mirror(b2), mirror(a2))) :: a1
         = ( (.NIL :: (b2 :: a2 ) ) :: a1

where these forms of identities are typical of derivations of the results for definite operands.  With experience, mixing of CFob canonical form notation in Ot expressions, as done here, is useful for readability.

The statements Mirror1-Mirror2 are by way of definition and constitute representation of the function that is characterized in this manner.  That is sufficient demonstration that there is such a function in Of, since Of is declared to include all functions on ob operands with results in Ob.  This is by definition of
    ‹ob› = 〈Ob,Of,Ot〉.

There is no inherent sense in which the mirror( x ) function has been represented correctly.  It is what it is.  I declare that representation via Mirror1-Mirror2 satisfies my intention for the function.  The decision to leave all singletons, including enclosures, intact is mine.  The use of singletons in the same manner as individuals will be common as an idiom in the crafting of functions on obs.

For mirror( x ) to provide a satisfactory mirror-image of an ob with respect to its pairings, it must satisfy the natural requirement that mirror( mirror( x ) ) = x.  That can be proven.

         ob.is-singleton( x )                                                    base case
            ⇒ mirror( mirror( x ) ) = mirror( x ) = x
         mirror(mirror( x )) = x ∧ mirror(mirror( y )) = y           induction step
   
           ⇒ mirror( mirror( ob.c(x, y) ) )
                     = mirror( ob.c(mirror( y ), mirror( x )) )
                     = ob.c( mirror(mirror( x )), mirror(mirror ( y ) )
                     = ob.c(x, y)                                                     
         mirror(mirror( x )) = x                                               by structural induction

This proof is by structural induction.   By design, the definition of ‹ob› primitive notions together with the partial-ordering relation ¶ satisfy the requirements for applicability of structural-induction.

  1. Here, the single base case consists of all singletons and that is straightforward.
  2. The induction step is by showing that when the two components of a pair satisfy the condition, so does the pair.
  3. There being no other cases to cover, the conclusion follows by structural induction. 

The important consequence of having a proof, different from a demonstrative example, is that we establish the condition for all possible operands by mathematical means.

Among experts, a proof might not be exhibited for this simple case, based on the understanding that the proof is easily constructed.  Here, the objective is to illustrate the nature, purpose, and benefit of the mathematical approach and more detail is provided.

1.3 On Equivalent Function Representations

  • aLast1.  ob.is-singleton( x )  ⇒ aLast( x ) = x
  • aLast2. ¬ ob.is-singleton( x )  ⇒ aLast( x ) = aLast(ob.a( x ))
  • blink1. blink( x ) = aLast(mirror( x ))

Here, aLast( x ) is the ob.a counterpart of bLast( x ).   blink( x ) is the same as bLast( x ) and, however  obvious that is on inspection alone, that can also be proved by deduction.

         ob.is-singleton( x )                                                     base case
             ⇒ blink ( x ) = aLast(mirror( x )) = aLast( x ) = x = bLast( x )
         aLast(mirror( y )) = bLast( y )                                     induction step
             ⇒ bink(ob.c( x, y)) = aLast( mirror( ob.c( x, y ) ) )
                     = aLast( ob.c( mirror( y ), mirror( x ) ) )
                     = aLast( mirror( y ) )
                     = bLast( y )
         blink( x ) = bLast( x )                                                 structural induction

We have demonstrated that blink and bLast, as defined above, are representations of the same function in the Of of ‹ob› = 〈Ob,Of,Ot〉.

It is commonplace to say that the functions blink and bLast are equivalent.   In rigorous speaking of the abstractness of mathematical entities it will be preferable, instead, to say that the function representations are equivalent insofar as the same function is determined.

Absent canonical forms for expression of functions in Of, assuming more about equivalent function representations is inappropriate although one might have a preference for representations that are expressive and simpler.  Demonstrations of equivalence also favor substitution of simpler representations for more complicated one.

When it comes to computational interpretations, on the other hand, there are only the function representations to work from, and derived computational interpretations may have material differences.   For example, one might prefer bLast( x )  over blink( x ), operationally (but maybe not if y = mirror( x ) is already “in-hand” and bLast( x ) is desired, making aLast( y ) more appealing).

2. Representing Other Structures: Boolean Algebras

Having data represented via encoding as obs was introduced previously.   Now we look at how one arrives at functions on such obs that honor the intended data representation.  We’ll start for the case where the representation is of some discrete structure other than ‹ob› and for which there already is a mathematical characterization.

Consider a specified abstract structure, ‹S› for which an interpretation in ‹ob› is desired.  What must be preserved by an interpretation of structure ‹S› in ‹ob› that is thereby amenable to computational-interpretation in the ‹ob› model of computation, are the essential functions of ‹S› represented in an effectively-computable form.

Boolean Algebras are mathematical structures that are interesting for computational purposes; they provide handy examples that demonstrate layering of representations and interpretations.


A characteristic of Boolean Algebras is that they apply over a variety of domains of discourse (i.e., other/related structures), yet the essential mathematical pattern of a Boolean algebra is exhibited in every case, typically in more than one way.


The axioms pertain to abstract, theoretical entities.  We can establish an effectively-computable representation directly by exhibiting function representations that are confirmed to satisfy the axiomatic specification.

2.1 ‹bp›: The Prototypical Boolean Algebra


Accomplishing effective-computability in ‹bp› given distinguished ⊥ and ⊤ offers a straight-forward interpretation in ‹ob›.   Just select two obs and corresponding representation of functions.


Restriction of the ob.NE.bp interpretation of ‹bp› in ‹ob› to two distinct Ob elements is awkward for computational-interpretation; it leaves undefined what would happen, in a computational model based on ‹ob›, when the restriction to those two operands is violated.  A remedy is offered with interpretation ob.p01.bp.


The basic technique of identifying domain elements across structures and then matching representations of primitive notions is illustrated with the ob.p01.bp interpretation of ‹bp› in ‹ob›. Careful identification of the interpretation ‹bp› in ‹ob› is akin to the approach used in demonstrating computational interpretation of ‹ob› in an SML/NJ abstract data type signature.

2.2 ‹ba›: General Boolean Algebra Representation

In what follows, the general case of Boolean Algebras on finite domains is addressed.  The treatment is more elaborate than for ‹bp›, involving the interpretation of other structures and arriving at interpretations in ‹ob› at the end.   Care is taken to identify the stages and transition from one to the next.

It is a remarkable characteristic of Boolean Algebras that many have interpretations in each other.  In consequence, there need be only a few representations of Boolean Algebras that suffice as interpretations of all the others; they will be effectively computable thereby, as well.

Here the outcome is a single ‹ob› representation, ob.bvx, that provides an interpretation for all finite Boolean Algebra cases.  The justification is essentially mathematical; ob.bvx does not make for a one-size-fits-all computational interpretation however; large-scale situations require more-elaborate computational interpretations.

We start with consideration of what are termed concrete Boolean Algebra representations: ‹bn› structures.

There is a handy means of representation of all subsets of a finite set of distinct elements.  Although not a concrete representation in itself, each representation under the scheme is isomorphic to corresponding concrete representations and thereby an entire family of Boolean Algebras.


The representation of ‹bvn› Boolean operators is abbreviated above, with the sequences all having the same length, n,  and operations extended onto corresponding pairs of list-operand elements.  The general pattern is to be understood as applying for every n.

The isomorphism of ‹bvn› with any concrete Boolean Algebra involving a set of n elements is straightforward.


Given a ‹bvnn-tuple, X, the indicator function Iai( X ) determines whether ai is a member of the corresponding (concrete) subset.

2.4 ob.bvx: One Interpretation to Hold Them All

By finding interpretation of any ‹bvn› in ‹ob›, we have represented the corresponding concrete Boolean algebra, ‹bn›, individually.  The representation ob.bvx, below, is a single formulation that provides interpretations of any ‹bn›  (and thereby, all of them) and hence all of the finite Boolean Algebras via isomorphism.

The ob.bvx representations are a bit more convoluted than the preceding ones, such as ob.p01.bp, in order to accommodate the necessary variability of interpretations without fixing n.  The trade-off is in having to develop and confirm the representation but once, rather than separately for each ‹bvn›.


Among the features of interpretation in ob.bvx, there is a canonical form that can be used in expressing individual vectors in a sometimes-compact variable-length form.


There are a few nuances to tidy up, along with considering how to tie back from ob.bvx to any ‹bvn› and thereby all of finite ‹ba› via isomorphism.


This article ends with some reflections and references to some supporting material.



Continuation

  1. Interpretation, Representation, Computation, and Manifestation
    Reprise and account for specialized concepts in Miser Project, setting up for representation of the computation model