Miser Project: Narrowing ‹ob› for Computational Interpretation

2019-11-05 Update: Complete Migration from the Wordpress version
2019-11-02 Update: Touch-ups with initial migration to Blogger
2019-01-19/21 Update: Be more careful with x ¶ y, referring to it everywhere as a (strict) partial-ordering.
2018-11-02 Update: Pointing out, in the Denumerability and Effectiveness portion of obtheory.txt that the partial ordering, x ¶ y, assures availability of structural induction for deductions about functions in Of.
2018-10-17 Update: Significant adjustment of canonical form notions in the obtheory.txt on Denumerability and Effectiveness.

Preliminaries

1. Hark! Is That a Theory I See Before Me?
   The first-order logic with equality notation for Ot, the mathematical theory for ‹ob›
2. ‹ob› Primitive Functions
   Mathematical characterization  of four primitive functions and allied primitive notions that establish the domain of discourse, Ob, in structure ‹ob› = 〈Ob,Of,Ot〉

1. Primitive Notions

All of the apparatus for characterizing the mathematical structure ‹ob› = 〈Ob,Of,Ot〉has been used, so far, to present a simple universe of discourse, Ob and essential characteristics of that universe in terms of its primitive individuals, enclosures, and pairs.

• primitive individuals
  that are introduced simply by being uniquely-named in form ob.NAME, with ob.NIL given so far (although non-primitive individuals will be introduced by other means)
• enclosures
  signified by terms of form ob.e( x ) where x is any ob and ob.e( x ) is the unique ob that encloses that x.
• pairs
  signified by terms of form ob.c( x, y ) where x  and y are any obs and ob.c( x, y ) is the unique ob consisting of the pairing of the particular x and y.

Each ob is fashioned as exactly one of those (so far).  The primitive notions also provides mathematical means for discerning conditions that an ob satisfies. 

• If z = ob.c(x, y) then x = ob.a( z) and y = ob.b( z )  and also x ≠ z and y ≠ z
• If z = ob.e( x ) then x = ob.a( z ) and z = ob.b( z ) and also x ≠ z
• If z is an individual then z = ob.a( z ) and z = ob.b( z ).

These conditions are sufficient to provide predicates that discriminate the flavor of any ob.

• ob.is-pair( z ) is true if an only if neither of ob.a( z ) and ob.b( z ) are z, which simplifies to ob.b( z ) ≠ z
• ob.is-singleton( z ) is true if and only if ¬ ob.is-pair( z ), which simplifies to ob.b( z ) = z
• ob.is-enclosure( z ) is true if an only if ob.is-singleton( z ) and ob.a( z ) ≠ z
• ob.is-individual( z ) is true if and only if z = ob.a( z )

Note that there is no ob, z,  for which z = ob.a( z ) with ob.b( z ) ≠ z and that will never change.
This informal description is consistent with the rigorous treatment expressed in the notation for Ot.
  

2. Informal Terminology

The function names ob.a, ob.b, ob.c, and ob.e are not particularly suggestive of anything.  In that respect, it is the theoretical characterization of them that gives their essential significance, make of it what we might.  That is intended.

In contrast, the terms individual, singleton, enclosure, and pair are suggestive of some intended significance beyond merely what there is to be gleaned from Ot alone.

It is the case that certain idiomatic purposes are reflected in the choice of those names.  It is important to appreciate that, theoretically, the chosen names are irrelevant despite their outside-of-the-mathematical-theory hinting of an intended application of ‹ob›.  There will be more of this.  It is important to keep in mind that such “intended interpretation” is more about why ‹ob› is formulated the way it is; it doesn’t qualify what the ‹ob› structure is, mathematically.  The mathematical entities involved are solely what is discernable from the characterization in Ot.
  

3. Positioning for Computational Interpretation

There is more to be said in conjunction with the primitive notions for drawing a solid connection with computation.

• Denumerable.  The obs can be counted and there are exactly as many of them as there are natural numbers, given by the progression 0, 1, 2, …, n, n+1, … .
• Effective. Ot characterizations of functions, F, in Of are such that deduction of F( x )  for x a given ob is tantamount to a procedure for computation of at most one particular ob y for which y = F( x ) and x is any specific ob. 
• Strict Partial-Ordering. Structural induction available for deductions concerning the representation in Ot of functions in Of.  This has obs be finite with every ob having a finite canonical form in Ot.

To accomplish that, the textual definition of ‹ob› in file obtheory.txt is extended.

Continuation

1. Representing  Data as Obs
   Expanding on the difference between a logical mathematical theory and computational interpretation, noticing that obs themselves can be interpretations of data, that interpretation being carried over to a computational interpretation.  SML is used to demonstrate one operational interpretation in a programming language.
2. Representing Functions in ‹ob›’s Abstract World
   Reasoning about functions on obs and then about interpretation of other structures by representation of functions in interpretations.
3. Interpretation, Representation, Computation, and Manifestation
   Reprise and account for specialized concepts in Miser Project, setting up for representation of the computation model