Miser Project: Representing Data as Obs

2016-10-18 Update: Strengthening the notion that obs can be data representations, via encoding, with such representations preserved by computational-interpretation of the obs.  Expressing canonical form is now aligned with the updated introduction in Denumerability and Effectiveness

2016-10-20 Update: Smoothing the narrative on data representation along with additional consistent use of “canonical form.”

2016-10-30 Update: Cover some loose ends about computational-interpretation of functional-notation in the OB.sig.sml selection.

The Miser Project conception is composed of a mathematical formulation along with demonstration of computational interpretations that satisfy the formulation via careful engineering.

The foundation of the conception is the mathematical structure ‹ob› = 〈Ob,Of,Ot〉that circumscribes the domain Ob with its primitive functions and an useful supply of individuals to establish mathematical counterparts of computational data.

Here continues the advance toward mathematical formulation of a theory of computation by considering the (computational) interpretation of obs as data.

Preliminaries

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

Standing in Abstraction

It is useful to entertain the notion that the ‹ob› = 〈Ob,Of,Ot〉universe of discourse consists of intangible, abstract entities: the obs (in Ob) and the (abstract) functions/predicates on obs (treated informally and jointly in Of).   Those entities have no material/concrete existence and any abstract “existence” is entirely given by ‹ob› through the logical theory, Ot.  Consider that the entities (so-called) arise entirely in language with their essential nature given by the formulation of ‹ob› expressed in the preceding installments.  Having attention on particular obs (and particular functions and predicates on them) is simply a way of speaking and not any kind of separation from ‹ob›.  

This way of looking at the abstract nature of  ‹ob›  emphasizes that one cannot infer anything about the mathematical entities that cannot be deduced via Ot, the explicit logical-theory formulation of ‹ob›.  In particular, however closely a concrete computational interpretation manifests – gives the appearance of – ‹ob›-ness, it is important to not confuse engineered artifacts and processes with the abstractions.  Recognition of the difference is important in comprehension of how apparent layering of abstractions is achieved by computational means and software engineering.

This separation between the abstract and the apparently-operational is illustrated by the conscription of obs for interpretation as data representations.

Demonstrating Computational Interpretation

A demonstration computational interpretation of ‹ob› using the programming language SML/NJ has been prepared as an SML/NJ Abstract Data Type.  Possible computational interpretations are confined behind an SML/NJ signature declaration that limits what can be exercised of the computational interpretation and through which manifestation is achieved.  

The SML/NJ signature declaration is insufficient by itself.  The additional requirements for valid computational interpretations are specified in narrative comments.

ob-2018-10-30-1437-OB.sig.sml-0.1.1-validity

The use of SML/NJ is incidental and extremely useful because of the ease with which this kind of computational interpretation can be demonstrated.   Other programming languages and methodologies will also be used.  Using this particular signature with SML/NJ and not entertaining equivalent SML/NJ alternatives is simply by convention for the SML/NJ demonstration of oMiser’s computational model.  

To nail down this demonstration of computational interpretation, the signature is combined with definition of an SML/NJ structure that completes establishment of the valid interpretation. 

ob-2018-10-15-1681-ob.sml-0.0.14-structure

Verifying validity of the interpretation depends upon knowledge of the SML/NJ language as it is applied here and upon correct operation of the SML/NJ software and the computer used.

The condition of validity is that for any deduction concerning canonical forms in Ot, the corresponding computational procedure in the interpretation is aligned by yielding the corresponding interpretation of the deduced consequence.

Even when everything is correct, it can be impacted by operational malfunctions and by resource exhaustion.   To this extent, the interpretation is contingent and empirical.  It is an accomplishment of engineering and not logic, despite the remarkable fidelity of valid interpretations in practice. 

It should be clear that the establishment of interpretation validity is, in this case, dependent on inspection of the SML/NJ signature and structure and arriving at empirical agreement on their validity as a computational interpretation.  In this instance, there is a prima facie case, absent any contradictory evidence.

One subject of the Miser Project is demonstration of  validation support using mechanical deductive procedures that are themselves verified to be sound.   Understanding how that can be achieved will depend, at bottom, on a successful empirical foundation, such as that offered at the oMiser level.   It is important to confine the foundation to something whose empirical validity is readily verifiable before bootstrapping to higher levels.   The SML/NJ demonstration is exemplary in that respect.

Concerning Data Representation

Canonical forms can be taken as interpretations of data via an encoding – some arrangement of an ob that corresponds to a defined encoding of data.  We say the understood encoding is an interpretation of the (abstracted) data with the happy consequence that a suitably-restricted computational interpretation of the obs will preserve an interpretation as a particular representation of data. 

  • That an ob has the form of a defined encoding does not imply that it is intended to be understood as such a representation ; however, when an ob fails to satisfy a defined encoding, one can conclude the ob is not such a representation.
  • Whether operations on obs having the form of a defined encoding preserve the obs being such such an interpretation as data depend on how the operations honor data-interpretation-preserving restraints. 
  • One way to assure that a data-interpretation is valid is by establishing functions that encapsulate the interpretation, not unlike how the interpretation of ‹ob› is accomplished via the general-purpose language, SML/NJ, using signature and structure agreements to encapsulate a computational interpretation of ‹ob›.

By way of example, one data interpretation could be as representation of numbers.  

  • Let ob.NIL represent number 0,
  • ob.e(ob.NIL) represent number 1,
  • ob.e(ob.e(ob.NIL))) represent number 2, and so on.  

That’s mathematically adequate; it’s rather clumsy as a way of recording numeric data for any general practical purpose although we will see such elementary forms of counting in simple applications of oMiser.

A more suitable interpretation might be as a representation of numbers in a binary notation.  Let ob.NIL represent the digit 0 and let ob.e(ob.NIL) represent the digit 1, the two binary bits.  Then use

  • ob.NIL as number 0,
  • ob.e(ob.NIL) as number 1,
  • ob.c(ob.NIL, ob.e(ob.NIL)) as number 2,
  • ob.c(ob.e(ob.NIL), ob.e(ob.NIL)) as number 3, and
  • ob.c(ob.NIL, ob.c(ob.NIL, ob.e(ob.NIL))) as number 4, and so on.

Here the binary representation proceeds 0, 1, 01, 11, 001, … the reverse of the usual way that binary numbers are written.  That’s still an encoding; one must look elsewhere for preference of one encoding over another.

There are many ways that encodings can be established in this manner.  Knowing what is being represented and the rule of encoding is not inherent to the obs.  Additional information on the intended interpretation is required. 

It is intentional that the preceding examples be unfamiliar, exaggerating the difference between intended data and data interpretation in ‹ob›.  This is akin to the accomplishment of data representations in digital computers where the representations of data all devolve to organizations of and operations on binary bits.

Do the Lindy Hop

Although it is inescapable that additional information is required to know the intended representation for an ob’s interpretation as data, there is a simple measure to gain greater expressiveness in encodings. 

obap-2018-10-16-1532-obaptheory.txt-0.0.29

Lindies are a particular class of individuals adjoined to Ob in ‹ob›.  They are simply distinct individuals with no other significance.  Any intention for them and choices among them are of no significance in ‹ob›.   Their computational interpretation, in the oMiser model, is simply as interpretations of individuals distinguished by their specific character strings.  Their intended significance in an encoding situation is similarly not addressed by ‹ob›.  Lindies are freely available to improve the expressiveness of data representations.

Streamlined Notation

Interpreting individual obs as data is accomplished on individual canonical forms, no matter how those obs might be formulated on some general pattern.   The straightforward expression of those canonical forms is aided using a specialized notation.

  • A primitive individual, with name of form ending in .NAME, such as ob.NIL, is expressed as simply .NAME (e.g., .NIL).
  • A lindy, designated by Ʃ’s’, is expressed simply s.
  • ob.e( x ) is expressed ‵ ( x ), where the parentheses can be omitted when x is not a pair.
  • ob.c( x, y) is expressed ( x ) :: ( y ) , where the parentheses can be omitted when x is not a pair and where the parentheses on ( y ) are always optional.
  • In this notation, :: associates to the right, so abc :: .NIL :: ‵ GHI expresses the same ob as abc :: (.NIL :: ‵ GHI), which expresses ob.c(Ʃ’abc’, ob.c(ob.NIL, ob.e(Ʃ’GHI’) ) ).

When all optional parentheses are removed, this notation provides a direct counterpart of canonical forms which are more compact and, with practice, more understandable.  This equivalent canonical form is identified CFob.

Here is the CFob expression for an ob that might be intended as a small dictionary, with all of the terms being lindies.
    
       (English::en) :: (Русский::ru) :: (日本語::ja) :: (Français::fr) :: ‵ default

The previous examples of encodings can be streamlined using CFob expressions:

  • .NIL for 0, ` .NIL for 1, ` ` .NIL for 2, … etc.
  • b0 for 0, b1 for 1, b0 :: b1 for 10 (2), b1 :: b1 for 11 (3), b0 :: b0 :: b1 for 100 (4), etc., with the order of the bits in the binary-numeral representation reversed as before.  Observe that there are two levels (at least) of representation here: first as sequences of bits and secondly the interpretations of those as (decimal) numerals.

In Sight of the Objective: Models of Computation

The illustration of ob-representation of data has just scratched the surface.   It is time to consider how one reasons about functions of ‹ob› = 〈Ob,Of,Ot〉and how the are considered to be effectively calculable in general and in service of data representations.  That supports unfolding the Miser Project’s applicative model of computation, oMiser. 

Although there are many unexplained technicalities and additional steps to take, there is a glimpse of the objective in how intended data representations are achievable.

The mathematical structure ‹ob› = 〈Ob,Of,Ot〉incorporates an abstract model, to be introduced in subsequent articles, of algorithmic computation that demonstrates the nature of universal computation and also emphasizes how the stored-program model affords cascading manifestation — boot-strapping — of higher-level abstractions via software engineering.   There is a hint of that in consideration of data representation.

We forego, for now, ideas of efficiency and expressiveness in order to first capture the essential character of stored-program computation, including how data representation and representation-honoring operations are accomplished with computational interpretations of ‹ob›.

Advertisements
Posted in Miser Project | Tagged , , , , , , , | 3 Comments

Miser Project: Narrowing ‹ob› for Computational Interpretation

2018-10-17 Update: Significant adjustment of canonical form notions in the obtheory.txt on Denumerability and Effectiveness.

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.

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〉

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 xz and yz
  • If z = ob.e( x ) then x = ob.a( z ) and z = ob.b( z ) and also xz
  • 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.

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.

Positioning for Computational Interpretation

There is more to be said in conjunction with the primitive notions to allow us to draw a solid connection with computation.

  • We require that the obs be denumerable.  They 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, … .
  • We require effective Ot characterizations of functions, F, in Of be 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. 
  • We exploit partial well-ordering of the obs to have structural induction available for deductions concerning the representation in Ot of functions in Of.

To accomplish that, the textual definition of ‹ob› is extended.

ob-2018-11-02-1313-obtheory.txt-0.1.2-Denumerability

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.
Posted in Miser Project | Tagged , , , , , | Leave a comment

Miser Project: ‹ob› Primitive Functions

Preliminaries

Characterizing the mathematical structure ‹ob› = 〈Ob,Of,Ot〉involves first-order-logic with equality as the project notation for expressing  an applied logic, Ot, in which Ob is the entire domain of discourse.   Predicates and functions (in Of) are also introduced by characterization in Ot.

Four distinct functions, along with equality, are sufficient to distinguish among all of the Ob obs.  It will be the case that all characterization of obs, including as transformations of other obs, will reduce to compositions of these functions and cases of equality/inequality. 

ob-2018-08-26-1030-PrimitiveNotions

The notions of individual, enclosure, singleton, and pair have their inspiration in the nested array work of Trenchard More and  the foundation structure of LISP by John McCarthy.  It is intentional that these structural characteristics are limited and simple.

An essential characteristic is that the primitive notions have the structure be closed and the primitives be total.  One cannot in any way “fall out” or “fall through” a primitive.  And if the operands are defined, so are the results, viewing the primitives as operations.  This tidiness will be valuable in demonstrating practical computational interpretations of the mathematical entities of ‹ob›.

The elaborate treatment of just this much is also indicative of how much one must assert to narrow the objects of discourse to ones that are suitable for underlying a model of computation.  And we are not there yet. 

At this point, it should be rather clear that mathematical treatment is rather different than construction of computer programs that embody a mathematical theory in some sense.   It is one purpose of The Miser Project to sharpen and clarify that condition.

Continuation

  1. Narrowing
    ‹ob› for Computational Interpretation

    Summarizing the primitive notions
    and positioning for computational interpretation with additional restraints
  2. 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.
Posted in Miser Project, Uncategorized | Tagged , , , , | Leave a comment

Miser Project: Hark! Is That a Theory I See Before Me?

2018-10-24 Update: Corrected definition of  ¬ p in the notation. (Yikes)

Once I have a stable experimental setup at the Spanner Wingnut blog, I will systematically revive my permanent, persistent blogs.  My agitation over the restoration of blogging and the use of hexo to generate static server pages reflects my anxious desire to restore Numbering Peano, the blog devoted to The Miser Project and related theoretical topics.

Pending restoration of Numbering Peano, I had begun writing about my capstone career project on a Facebook Page and on GitHub, where there are also preliminary (mock-up) demonstrations of implementation.  Issues on the GitHub project have been used to address questions and provide preliminary documentation.

At the moment, documentation is in plain-text files on GitHub.  That may continue as an ultimately-dependable form of persistent record.   When the hexo-generated pages are reliable, that will have the additional advantage of formatting with images and, most-important, formulas.   Mathematical notation expresses the bridge between the mathematical theory and the operational computation system for Miser.  Web pages can be arranged to do a better job.

At the moment, reliance on mathematical notation is confined to text and the use of Unicode encoding of the text.   Without the notation support for blog pages, the most reliable means of presenting the plain-text form on the web is via images.

ob-2018-10-24-0929-obtheory.txt-0.1.1-Notation

Having web pages and others, expressed in the GitHub MarkDown notation, allows for greater expressive power.  Text has, within its limitations, useful control over layout.  We’d like both, and wrestling the hexo-generated pages into a stable form, with support for mathematical formulas, is the chosen avenue.

Continuation

  1. ‹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〉
  2. Narrowing ‹ob› for Computational Interpretation
    Summarizing the primitive notions and positioning for computational interpretation with additional restraints
  3. 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.
Posted in Blog Development, Golden Geek, Hexo, Miser Project, Numbering Peano, Spanner Wingnut, Toolcraft | Tagged , , , , | Leave a comment

Returning to the Moon: Fire Suppression

I have relied on RSS feeds for all of my blogs, including this one, and collecting blog posts of others.

It was satisfying to enable  an RSS feed on the experimental hexo-generated blog now at Spanner Wingnut’s Muddleware Lab.

As part of the PC repaving mentioned the other day, it dawned on me that I have no RSS feed reader installed any longer, and I have no idea if I preserved the history of the discontinued FeedDemon Pro software that I had kept limping along for years. 

I had it in my head that I had failed to backup the FeedDemon database someplace separate from my system drive.  Either way, I chose to reinstall FeedDemon so that I could at least see recent blogs and, especially, confirm the Spanner Wingnut blog hexo-generated RSS feed.

FeedDemon installed with an empty database, and I did find one on my D:\ drive, the one unaffected by my reformatting and reinstall on my system drive.  It took me a bit to realize that this is all called “cache” and the FeedDemon File | Manage Cache menu item allows me to switch to the previously-operated cache. 

Restored FeedDemon restores history and finds recent posts

The current RSS content from Spanner Wingnut is also found, and the plaintext is correct, though not with the exact styles.   On linking to a post, the known Internet Explorer rendering failure is exhibited.

FeedDemon uses Internet Explorer for its internal web browser, exhibiting the same problems when Internet Explorer is used directly.

There’s no escaping this issue, and here’s a case where I can’t control what is used for embedded viewing of blog posts.

I thought I might learn something by viewing the oldest Spanner Wingnut post through the feed.  Not a chance.   Hexo regenerates all pages when it regenerates any of them, and past evidence of something different is eradicated.

I will blunder along.  It is becoming pressing to have the experimental blog stabilizes so that I can replicate the generation scheme for production blogs that it’s urgent to re-activate.

Posted in Blog Development, Hexo, Spanner Wingnut | Tagged | Leave a comment

Returning to the Moon: Escape Tower Incident

There have been a couple of setbacks in my efforts to restore self-hosted blogging capability.  I found a browser/server incompatibility that breaks my brain.  And then I had to do a fresh system drive and operating-system reinstall on my main, development PC.

Browser/Server Flummox

The hexo-generated Spanner Wingnut experimental blog seemed to be going great guns.

The blog appears correctly in Edge and Chrome

Apart from some simple style adjustments, the experimental blog seemed ready for customization and revitalization of my “production” blogs.

Everything works well under local testing and on the live location, using Google Chrome and Microsoft Edge.  The local server also displays properly using Internet Explorer.

The hosted web fails to be browsed properly using Internet Explorer, though.

The page display is completely ruined when using Internet Explorer to access the web-hosting site, but not the local machine server

The complete failure is with Internet Explorer only when accessing the hosted site.  That is completely baffling.

  • It is conceivably a server setting problem, perhaps something to do with MIME types of served content or even something in the formatting of CSS and JS components.
  • It is unacceptable that the site not be viewed properly with what remains the default browser for many users.
  • It appears that the image formatting is a problem, but I notice that the styles for remaining parts of the page are also disrupted.
  • There is nothing revealing when viewing the HTML served up by the hosting site.

My failure in not testing the deployed site in Internet Explorer from the beginning means I don’t know what customization changes first produced this result.

I am willing to remove the top-page image and simplify the top banner, in hopes that eliminates the difficulty. 

I am gathering myself for digging into that.  But first, … .

System-Restoration Priorities

While I was scratching my head over the browser/server failure being limited only to remote access by Internet Explorer, I managed to crater my system SSD drive.   Fortunately, I was able to use a recovery USB drive to get Windows 10 back in operation on a clean SSD.  Also fortunately, all of my data, and some installed programs, were on my D: drive, not the C: system drive.  I also had the good fortune to have code backups (GitHub) and data backups (OneDrive plus an attached USB-connected drive).  Also, many software subscriptions (Office 365, Steam, Cakewalk SONAR, etc.) make it very easy to restore software and, usually, my latest configurations and status.

I have gradually been re-installing software, starting with essential programs for everyday operation, such as Microsoft Outlook on the desktop. 

I have now successfully re-installed node.js and hexo.  The GitHub connections of my working nfoCentrale blog folders were already restored.  Now it is time to have the FTP deployment working again. 

With that last step, I can work on curing the Internet Explorer browser/server failure.

Software Engineering for Everyone

Software engineering is about having reliable processes for making dependable delivery and lifecycle support of computer software.  

There are some elements to computer-aided production and operation of blogs, and web sites generally, that pose tool-chain, workflow, and testing/analysis problems that are very unlike development of standalone PC software. 

My engineering of a dependable blogging-engine authoring mechanism requires quite a bit more software-engineering practice, simply for myself.   I need to look at how I am not creating practices that measure up to my own expectations for dependable operation.

Posted in Blog Development, Hexo, Spanner Wingnut, Toolcraft | Tagged , , , , , | Leave a comment

Returning to the Moon: Launchpad Security Penetration Exercise

There is an unexpected reward for moving source-code management of my Hexo-generated blogging to git and GitHub.  GitHub provides dependency analysis of node.js projects.  I receive an automated email about one dependency of my hexo-spanner code.

GitHub analysis of the hexo-spanner package.lock.json package reveals that UglifyJS2, depended on by Swig, has a known security vulnerability cured in a later version.

The uglify-js package is only depended on by Swig.  That places it in isolated use in confined ways under hexo.  I (will) do nothing to rely on Swig in any other manner.    I’ve dismissed the alert with explanation that the reported dependency is not exposed to the exploit.  I also created an issue on the hexo GitHub wondering if Swig can be deprecated from use in Hexo, since Swig is no longer maintained.

All in all, an amazing reward of my transposition of the Spanner Wingnut source-code management to GitHub.

Posted in Blog Development, blogs, Git, Hexo, Security Vulnerabilities, Spanner Wingnut, Toolcraft | Tagged , , , , | 21 Comments