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.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.
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
- Hark! Is That a Theory I See Before Me?
- ‹ob› Primitive Functions
- Narrowing ‹ob› for Computational Interpretation
- 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.
- 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 ))
- 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 )) )
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.
- Here, the single base case consists of all singletons and that is straightforward.
- The induction step is by showing that when the two components of a pair satisfy the condition, so does the pair.
- 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
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.
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.
2.4 ob.bvx: One Interpretation to Hold Them All
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
- Interpretation, Representation, Computation, and Manifestation
Reprise and account for specialized concepts in Miser Project, setting up for representation of the computation model
