Version
0.03 Last
updated 2002-07-10-11:18 -0700 (pdt)
The latest version of this document is always at http://Miser-theory.info/sketch/osketch.htm.
For a history of this document and its revisions, see Miser Note N020600:
Miser Sketch Notes.
Here is a sketch of the foundation for any
(and every) Miser system. This is the oMiser level because it
covers the elementary, ‹ob› structure only. It is devoted
exclusively to Obs, seemingly alone in a world unto themselves. This simple, closed structure is at the foundation of all
extensions that are introduced to achieve "higher" levels.
oMiser and ‹ob› provide a rich yet spare environment. oMiser is the launchpad for distinguishing how much we rely on the familiar and how much is overlooked in our everyday approach to computation, theories, logic,
mathematics and especially to language itself.
Content
[TYPOGRAPHY WARNING: This document uses
HTML entities for special characters, such
as ¶ and similar symbols. Most of them will render properly in all current
browsers. However, some character, such as ¹
(not-equal from the Symbol font) and ‹ (left-pointing-single-guillamet
from the Windows font) may not render well at all. It is the intention
to use Unicode for this and related pages, and also use MathML styles.
That has not been done and you may have difficulty rendering the present form
of this document as intended. -- dh:2002-07-05]
We want to put something up top about what we are doing here, and the
viewpoint that we want to encourage. [These are some loose notes until
there is more structure. -- dh:2002-07-03]
Two ways we want to look at Obs and the basic provisions of the
Miser system.
We have a computer implementation in mind. But it is
abstracted. Still a computer implementation, but not a fixed
implementation. So I will illustrate the computational nature of Miser by
informal means: diagrams, descriptions of behavior of a computer, and so on.
At the same time, there is also a theoretical system, a
mathematical structure, that the computational system honors in a particular
way.
I will give informal characterizations of the computational
system, using diagrams that are to be suggestive of valid interpretations
of the theory.
I will also give informal expression to the theoretical system
of which the computational system is to be a valid interpretation.
This illustrates how these two views can be brought together in
demonstration of what it means to manifest abstractions (theoretical entities) by
computational means. This sets the stage for a rigorously developed
manifestation in operational computer software and for a formally developed
exploration of the theoretical system that is its foundation.
It is important to notice that the theory is being developed with a
computational interpretation in mind. I am interested in the operational capabilities of
the kind of system that I envision, while at the same time the development of a
theoretical system sharpens understanding and also provides a venue for
exploring the way that theory and reality can be said to collide in the
computer. The egg and the chicken have no existence apart.
[This is turning into a
hodgepodge of mixed levels of description and incoherently-connected
concepts. It will be like that until some organization emerges where I
can put the less-essential but later-significant material off to the
side. Meanwhile I do this to gather my forces and ensure that the
sketch that is distilled out remains consistent with what is to follow or
expand on it. I will also begin separating the sketch into multiple web
pages, probably on a major section basis, as those sections become complete
enough to move onto pages of their own. The sketch will have a
drill-down quality to it. -- dh:2002-07-05]
We mean by this that Obs are
sufficient. In principle, we don't need anything more to provide a
universal system of computation. It is neither practical nor desirable to
limit ourselves this way. We start here because this is the place where we
can reveal exactly what is involved in manifesting anything via computation and
then what is or is not remarkable by extensions that deliver computation on
more-familiar terms that, nevertheless, preserve Obs and their power.
1.1 Identity and Existence
|
Here it is argued that comparison, knowledge of existence, and understanding
of number, are essential to knowledge, but cannot be included in perception
since they are not affected through any sense organ.
|
-- Bertrand Russell on Knowledge and Perception in Plato.
[This section provides a basic flavor of the approach and how we
will toggle between several perspectives, always endeavoring to keep them
distinct. -- dh:2002-07-03]
1.1.1 Theoretical Structure
The
structure, ‹ob› = ‹Ob, Of, Ot› consists of
-
a collection, Ob, of elements (the individual Obs),
-
a collection, Of, of functions over Ob
-
and a (semi-) formal system, Ot, with initial axioms
that provides everything and only what there is to be (semi-) formally known about
‹ob›.
We are intentionally allowing ourselves to be obtuse about Ot and whether
it is properly in or of the structure ‹ob›. We are not even clear on what it means to say
that ‹ob› is a "structure." We will leave it that way for now and tidy up
later.
Something to deal with almost immediately is having it be clear when we are
talking in our own language about the structure ‹ob›, and when we are somehow speaking within the structure
‹ob›, and if it even makes sense to consider that one can speak that way.
Keeping track of the multiple levels of language (our language, the metalanguage,
the formal language, etc.) is important because we will identify features of ‹ob›
that are themselves linguistic in character.
For now, this is just something to notice that may not always be
obvious. We'll improve on that as we go.
[I want a picture or diagram about the relationship of theories and
interpretations to pave our way here. The key thing is that reasoning and
deduction in the theory gives us some power regarding the
interpretation. I keep wanting to do it later, but it seems that some
initial depiction is necessary to build on as we acquire more theoretical
content. -- dh:2002-07-05.]
1.1.2 Informal Conception
There are Obs. That's all we know for
now. Don't assume anything. And don't confuse the notion of Obs with
anything that you might already know about objects or "objects" or
object-oriented programming or anything else. We'll look for prospective
connections later. Consider that, with oMiser, Obs have no
relationship to classes and objects the way they are spoken of by software
developers. Although a relationship to classes and sets in logic and
mathematics is inescapable, I ask you to set that aside too. We'll
put it in later.
For
now, there is very little to know about Obs. They are some kind of
abstraction. We will indicate how little we know by depicting an
arbitrary Ob as a cloud-like entity.
It is fundamental that there appear be many Obs -- an unlimited
number, actually -- and
however they come to
our attention, they are distinguished in some way. When the same Ob comes to our attention in more than one way,
it is always recognizable as the same Ob. That's an essential quality for all interpretations that we
want to allow.
This conception is reflected in the theory by the rules for identity
and distinction. It is not a complete formulation and we will ultimately
give this topic much closer scrutiny.
I said, "There are Obs," as if Obs are. It
is a way of speaking. It is not that Obs are real or that ‹ob›
can be found somewhere in physical reality. It is more like,
"consider that there are Obs." There is no commitment
other than to give Obs a kind of theoretical standing, to speak theoretically. Later, when we have more foundation under our belts, we can
look to see in what ways, if any, Obs may be "more real" than that.
There are no Obs except in this intangible sense in which we
speak as if they are. The theory gives us a way of speaking correctly
about Obs (since there is no way other than speaking -- including reading and
writing -- that we have for mutually envisioning what their
characteristics are, even conceptually), and we will use the language of theorizing just that
way, in speaking of ‹ob› and the qualities of Obs.
[I have
specifically omitted demonstration with a computer as a way of speaking about or
conveying something about ‹ob›. This is worthy of a note, at
some point. I intend to address that case, but I am not prepared to claim
it just yet. -- dh:2002-07-05]
Speaking of ‹ob› and the Obs is to be taken as an act
of invention, even though we use the language of description. The
descriptions are free creations, yet they are not arbitrary. There
is a logic to them. We use the notations and concepts of mathematics and
logic to provide consistency in our speaking of Obs and ‹ob›.
That consistency stems from
our fundamental premise: ‹ob› is lawful.
That is to say, we assert that ‹ob› is lawful, and that the
rules of logic apply and prevail. That is a rule of the game of ‹ob›.
As the author (and referee) of the game, I'm giving that to you as the rule. If we find that there is
something inconsistent in the descriptions that are made, it is an error in the
descriptions and conceptualizations, not in the fundamental premise. No mischief is permitted in that regard. Any mistakes
that violate that condition will be repaired and the premise restored.
That's the nature of the game. It may turn out that this is a game we
cannot win. We will only know through the faithful playing of it.
We are learning to speak using the language of logical
theories. Our demands on logic are simple at the beginning and we will
start out with informal and familiar styles of equations.
Let us begin with the first layer above the fundamental premise:
that of identity and distinction. We will pay more attention to the
conceptualization and the formalization of existence after that.
One thing to pick
up on later is that it is the structure that is the "whole" and when
we have our attention on individuals, speaking conceptually or in the language
of the theory, that should be taken as a way of viewing aspects of the
whole. Although we speak of individuation, and might speak of Ob as a set, it is
not that Obs (that is, the members of the conceptual set, Ob) are independent
entities. The obs are interdependent and inextricable with the structure, ‹ob›. Everything else is a difficulty of
language. Quote [Quine1969].
1.1.3 Identity for Obs
|
Consider an arbitrary integer, p. For example, q.
|
-- told to me in the 60s by one of my many language-loving friends
1.1.3.1 There is an identity relationship among the Obs We
borrow the common
symbol "=" for the relationship of Ob identity. 
We
will use the symbol in a way that makes it clear when we are referring to Obs
and when we might be referring to something else where a similar notion of
identity might apply.
1.1.3.2 The
intended interpretation of x = y is that Ob x is Ob y.
1.1.3.3 Reflexivity. If x is an Ob, x = x.
1.1.3.4 Symmetry. For any Obs x and y, if
x = y, then y = x.
1.1.3.5 Transitivity. For any Obs x, y
and z, if x = y and y = z, then
x = z.
1.1.3.6 Distinction. x ¹ y is
equivalent to ¬(x = y) by definition, where
"¬p" signifies "not p." The intended
interpretation of x ¹ y is that Ob x is not Ob y,
which is to say that Ob x and Ob y are distinct.
1.1.3.7 Identity Completeness. For any Obs x
and y, it is the case that x = y or x ¹ y.
1.1.3.8 Identity Consistency. For any Obs x
and y, it is the case that ¬(x = y and x ¹ y).
1.1.3.9 The identity-completeness and
identity-consistency conditions place a strong requirement on any valid
interpretation of ‹ob›, and are part of the assurance of a sound computational manifestation for Obs.
It is usual to place/demonstrate these conditions at the level of (or about)
the overall theory itself. Whether or not we will do so, the conditions
are established for identity of Obs. [Find a better term if "sound" is inappropriate or misleading
here. Also, look at what it is to assert consistency and completeness in
this way as statements of ‹ob› theory, Ot.]
1.1.3.10 Consequences of Formality. Here we begin to see the
consequences of formal expression of a theory. Notice that the
characteristics of identity (1.1.3.3-1.1.3.6), used in some form since the
time of Euclid, would be ridiculous if we were speaking of definite, determined
things. In that case, identity and distinctness are confirmable in our
experience or by some empirical inspection or confirmation. A statement
such as x = x would then seem unnecessary or, at best,
trivial.
[Put in that we
are beginning to describe appropriate inferences among formal
expressions. An appropriate reading of x = x,
for example, is that any any form of this pattern where x is some
formula for an Ob is to always be true in the theory. The axiom, 1.1.3.3
is required because it actually arises in chains of inference about the
identity of Obs. So the obvious needs to be made explicit. More
significantly, this simple condition is often violated in computational
systems. That is, we use expressions for computation for which 1.1.3.3
fails, yet we reason about computations as if it doesn't. It is my
profound desire to avoid that nonsense and, indeed, demonstrate that there is
no reason to tolerate it. We will produce far superior and reliable
computational results as a consequence. --dh:2002-07-05]
1.1.4 Distinction Among Obs
1.1.4.1 We use x ¶ y to
signify an ordering relationship among the Obs. The intended reading of x ¶ y
is that Ob x is
prior to Ob y. An important consequence is that if x ¶ y,
then Ob x must be distinct from Ob y.
1.1.4.2 [Irreflexivity] For any Ob x,
¬(x ¶ x).
1.1.4.3 [Asymmetry] For Ob x and Ob y,
if x ¶ y then ¬(y ¶ x).
1.1.4.4 [Transitivity] For Ob x, Ob y,
and Ob z, if x ¶ y and y ¶ z, then
x ¶ z.
1.1.4.5 [Distinctness] For Ob x and Ob y,
if x ¶ y then x ¹ y.
1.1.4.6 [Identity Distinctness] For any Obs
x
and y, it is the case that
x
= y if and only if ¬(x ¶ y or y ¶ x).
This is an unusual notion of distinction. Section
1.1.3.6 provides the usual notion, where distinction is merely x ¹ y
with it becoming possible to infer more cases as constants, functions, and
axioms about them are introduced.
[Introduce something about the difficulty of inference, and
illustrate the kinds of inference we can make in this case. This is
definitely the case of having a particular computational/constructive
interpretation in mind. Maybe something about applied (equational)
logic.]
1.1.5 Computational Manifestation of Obs
[Rework this part to have it that manifestations are erected
and discarded as part of computations, but it is as if ‹ob› is
always there. The manifestations preserve this illusion. Also,
make it simpler and not so heavy. Finally, point out that it is an
oMiser software library that provides the necessary manifestation.
Later, we will even consider that, among all computers on which some
manifestations of ‹ob› are realized, there is every indication that
it is the one and only ‹ob› structure anywhere. We get to look at the
Platonic illusion. This may belong in separate notes, but I want to
remind myself to keep my use of language consistent with that prospect.]
Obs
will be represented in the processes of conventional digital computers.
This is accomplished by organization of computer memory and software in such a
way that Obs are manifest in the operation of the digital computer.
Manifestations are established using oMiser software libraries
provided for use by computer programs on a variety of different computer
systems. The library
procedures deliver interfaces to manifestations of Obs. The
operations available at the interfaces behave is as if the Obs are actually
present somewhere "behind" the interfaces of the manifestations. The manifestations
operate successfully as representatives of the Obs in the processing environment of the
conventional computer system.
In the implementation of oMiser, the manifestations are
delivered to other software by the oMiser library procedures. It
is done in such a way that the manifestation is successful and the developers
of the other software can trust in that fact. There is also a software
program, oFrugal, that uses the oMiser library and delivers access to ‹ob›
(as manifested) by interaction with the computer's user or operator. We
will see below (section ???) that this is yet-another-manifestation and that
it confronts us with the formal nature of computer operation at the boundary
between computer interface and human operator.
In the delivery of manifestations within the common
computational model, a computer storage location typically serves as a placeholder
for a manifestation. The storage holds a man-handle of some kind.
The man-handle serves to locate a particular manifestation (interface).
Man-handle storage elements are the means to keeping track of the Ob
manifestations that a computer program is accessing.
In an operating computer system, different man-handle storage
might refer to the same manifestation interface. Different interfaces might
provide manifestation of the same Ob. The form of identity maintained for
computer storage, interfaces, and handles to interfaces is generally
independent of the identity and distinction among the manifest Obs -- there
are different worlds or domains involved.
Part of a particular manifestation methodology is provision of
an oracle that can confirm whether the manifestations accessible
through two manifestation interfaces or two man-handles are for manifestations
of the same Ob or
not. oMiser provides such an oracle. That is, the identity of the
manifest Obs is always determined. [Watch that language.]
The possession of a valid man-handle to a manifestation
interface establishes the (virtual) presence of the particular manifest Ob. Obs
(may) have persistence beyond the existence of any manifestation and can reoccur
as the Obs of subsequent manifestations. When we have a man-handle, we
say that the Ob is determined. Much of what we say about the
computational model revolves around an Ob being determined. There are
operations that one can carry out with manifestations where an Ob cannot be
determined, and no result is delivered. That is to say, oMiser never
delivers a man-handle for a seeming manifestation that has no determined
Ob. It just doesn't happen. We will discuss later what happens
instead, if anything.
We will again
discuss the notion of determined Obs when we look at computability of the
functions, Of. It will be important to make this a very sharp
notion. Until then, we entertain the idea of a determined Ob in an
informal way.
At this point, you might say that the software that provides
for manifestation of Obs is successful at perpetuating the illusion that there
is an Ob "there, somewhere," simply by ensuring that no behavior can
be elicited that would contradict that illusion.
One might also say that there is a valid interpretation
of ‹ob› in the operational behavior of the oMiser computer
software.
One could also say that oMiser represents ‹ob›
in the computational model of the computer system.
We will prefer to say, in the common manner of computer
science, that oMiser (actually, all of the oMisers) implements or realizes
(that is, manifests) ‹ob›.
These perspectives are pretty much interchangeable at this
level of conceptualization. I prefer realization, with no existence
commitment more than that it is indeed a successful illusion.
1.1.6 Existence and Interpretation
[This section requires much work. We want to talk about
the requirements of formalism that apply, and we want to talk about
interpretation. A diagram would be of great help. These notes
include fragments from elsewhere. -- dh:2002-07-05]
Requirements of Formality. [Clean this up between
the beginning, sections 1.1.3-1.1.4, and here.] Here we begin to see the
consequences of formal expression of a theory. Notice that in some sense,
the definitions and axioms (1.1.3.2-1.1.3.5) of identity, used in some form ever
since Euclid, would be ridiculous if we were speaking of definite, determined
things. In that case, identity and distinctness are confirmable in our
experience or by some empirical inspection or confirmation. These
statements are not about the things, but about the logical formalism by which we
are expressing what there is to say about the theoretical structure, ‹ob›,
abstracted from whatever actualities might be available, if any.
Talk in the computational and informal conceptions first.
This is a place to talk about using the language of theory to have our attention
on Obs without ever seeing one. And then that we get to make inferences
about them, still without having to see one.
We assert that the
definite, determined object ob-NULL
is an Ob.
Later, we get to look at how manifestation of ob-NULL
(or any other, but this one is assured) gives rise to all of ‹ob›,
that Obs live only in ‹ob› (as it were) and are not reduced or separable. This
is a risk because we can formally separate Obs (e.g., by writing (canonical)
expressions for them). This confusion is to be avoided.
1.2 Basics - Informal Theory
[Here provide some standard information about Obs and the a-part
and b-part functions of obs. A diagrammatic presentation of some typical
Ob(s) will be employed to make our point.
We don't know exactly where we will introduce that. We
will actually deliver functions a and b first, then go into other cases.
ob.a(z) = z or ob.a(z)
¶ z
ob.b(z) = z or ob.b(z)
¶ z
If ob.a(z) = z, then ob.b(z)
= z.
1.2.1 The set of Obs is closed with respect to the
primitive Ob functions ob.a, ob.b, ob.c, and ob.e. The primitive functions are
well-defined and total.
1.2.2 The individuals, singletons, and combinations
partition the Obs. Every Ob is exactly one of these.
We need to motivate the peculiar notation ob.a and also
discourage people from confusing it, at this point, with notations of
object-oriented programming systems. (I haven't chosen whether to use
bold-face or not, at this time.)
[There is something
interesting in the way we look at Obs as kinds of rooted trees. It would
appear that there are no inverses for the functions ob.a and ob.b. This is
a curious thing with regard to statements I am making about ‹ob›
being inseparable. I am not sure where or whether it matters to introduce
that. -- dh:2002-07-05]
1.3 Combinations
1.3.1 If z = ob.c(x, y), then
ob.a(z)
= x and ob.b(z) = y and z is a combination.
1.3.2 For any Ob z, z = ob.c(ob.a(z),
ob.b(z)) if and only if z is a
combination.
1.3.3 We define is-combination(z) to be
equivalent to the proposition that z = ob.c(ob.a(z),
ob.b(z))
ob.c(x, y) = ob.c(m,
n) if-and-only-if x = m and y =
n. This is
the ordered-pair condition. [Quine1969]
If z = ob.c(x, y), then x ¶ z
and y ¶ z.
1.4 Singletons
If z = ob.e(x), then ob.a(z) =
x and ob.b(z)
= z.
1.1.1.6 For any Ob z, If ob.a(z)
¹ z and ob.b(z)
= z, then z is a singleton and z = ob.e(ob.a(z)).
If z = ob.e(x), then x
¶ z.
ob.e(x) = ob.e(m) if-and-only-if
x = m.
We define is-singleton(z) to be equivalent to the proposition
that z = ob.e(ob.a(z))
1.5 Individuals
1.5.1 For any Ob z, If ob.a(z) =
z and ob.b(z) = z, then z is an individual.
1.5.2 We define is-individual(z) to be equivalent to the
proposition that z = ob.a(z). (This is
sufficient by virtue of 1.2.)
[Note that we have enough to tell, in the theory, that we have
an individual, but if there is more than one of them, this is not enough to tell
us which individual we have our attention on. We handle this with
¶ as a way to express, in this applied theory, that the constants we use
are for individuals and they are for different individuals. -- dh:2002-07-08]
1.6 Why It's All We Need
We express the idea that Obs are equivalent to expressions or
numbers or some form of carrier for other things. That is, Obs can be
employed as elements of formal expression, and they are as rich and capable as
any, even though not what we would normally think of.
This will get to enumerability and some related matters.
We generally go right to the demonstration that Ob interpretations can
themselves be interpreted.
Demonstration of countability and of formal adequacy will be
done by simply providing a grammar for formalization of Ob that accounts for all
the Obs there are.
We won't have a satisfactory resolution of the role of
individuals at this point, except the appeal of having an arbitrary supply of
them will be recognized as a benefit in comparison with working over a fixed
alphabet.
It might be useful to introduce a diagram for (formal)
interpretation just as we will have for theory interpretation.
We have described all of the primitive functions of ‹ob› but
two. It is asserted that these functions, with =, provide a
complete theory for Obs, given some way to characterize all the effective
procedures that there are on Obs.
2.1 The Apply-Eval Functions
2.1.1 The Universal Functions in Of
We are going to define two functions that we assert are in Of.
We signify that with this notation in theoretical language:
2.1.1.1 ob.ap: Ob × Ob ®
Ob is in Of.
2.1.1.2 ob.ev: Ob × Ob × Ob ®
Ob is in Of.
We express the nature of these functions in the following way:
2.1.2 ob.ap Definition
ob.ap(p, x)
= if is-individual(p)
then oApInt(p, x)
else if is-singleton(p)
then ob.a(p)
else oEvForm(p, x, ob.a(p),
ob.b(p))
The intended interpretation of ob.ap(p, x) is
as the application of the function expressed (or coded) in Ob p,
taking Ob x as that function's single operand.
| procedure p |
ob.ap(p, x) |
Notes |
| individual |
oApInt(p, x) |
the applicative interpretation of individual p
with argument Ob x |
| ob.e(c) |
c |
the constant result, c |
| ob.c(rator, rand) |
oEvForm(p, x, rator,
rand) |
the evaluation of the applicative form p with
a-part as operator and b-part as operand |
2.1.3 oApInt Definition
oApInt is an auxilliary function for the definition of ob.ap.
The key purpose is to assign to each individual an associated function, f: Ob ®
Ob. [It is important to note that this is an interpretation,
realized using the function oApInt. It is not that the individual Ob is
a function.]
Every individual Ob has an applicative interpretation. The function
designation oApInt(p, x) applies the applicative
interpretation of individual Ob p to the Ob x and yields
whatever Ob, if any, is determined by that applicative interpretation.
[We might later become comfortable saying that the form oApInt(p)
is the interpretation, and oApInt(p) x is its
application. That is the direction we are going, but we will hold back
for now. --dh:2002-07-08]
It is not necessary that every applicative interpretation be
determined. Another way of putting it is to say that oApInt is a partial
function.
[We will quickly deal with the ambiguity of there being an applicative
interpretation for every individual Ob p and the interpretation not
being determined.]
The following applicative interpretations are given:
| individual p |
oApInt(p, x) |
Notes |
| ob-NULL |
x |
the identity function on Obs |
| ob-SELF |
[tbd] |
[tbd] |
| ob-ARG |
[tbd] |
[tbd] |
| ob-A |
ob.a(x) |
the a-part of Ob x |
| ob-B |
ob.b(x) |
the b-part of Ob x |
| ob-C |
ob.c(ob-C,
x) |
ob-C
combined with x |
| ob-D |
ob.c(ob-D,
x) |
ob-D
combined with x |
| ob-E |
ob.e(x) |
the singleton consisting of x |
| ob-F |
[tbd] |
[tbd] |
| ob-G |
[tbd] |
[tbd] |
| . . . |
|
|
The names of constants for distinct individuals are not important to the
theory. The names have been chosen as an aid to us in remembering the nature
of their applicative interpretations (or other interpretations). The
individuals that are essential for ob.ap to provide a complete
computational model for Ob are ones with applicative interpretation ob.a,
ob.b, and ob.e. It is inessential whether the others have
known, useful applicative interpretations or not.
2.1.4 oEvForm Definition
oEvForm(p, x, rator, rand)
= if rator = ob-D
then if ob.ev(p,
x, ob.a(rand)) ¹ ob.ev(p,
x, ob.b(rand))
then ob-A
else ob-B
else if rator = ob-C
then ob.c(ob.ev(p, x, ob.a(rand)),
ob.ev(p, x, ob.b(rand)) )
else ob.ap(ob.ev(p, x, rator),
ob.ev(p, x, rand) )
It is intended that there be no special forms other than these. That
is, it the use of ob-D
and ob-C
here is to be the only exception to the ob.ap evaluation of an ob.c(rator,
rand) form. Ever. [That is so the reading of Obs as
formulae never changes as we expand beyond oMiser. This is actually a
tentative situation, and we might not be able to enforce this. I have no
exception in mind except for the possible explicit indication of a
tail-recursion operation. At some point, there needs to be an oracle for
determining whether or not a special form is in hand. This would allow
more exceptions without having to know all of them. We are not ready to
deal with that just now. -- dh:2002-07-08]
| rator |
oEvForm(p, x, rator,
rand) |
Notes |
| ob-D |
If ob.ev(p,
x, ob.a(rand)) ¹ ob.ev(p,
x, ob.b(rand)), then yield ob-A
else yield ob-B |
if the two parts of rand evaluate to different
Obs, return ob-A,
else return ob-B |
| ob-C |
ob.c(ob.ev(p, x, ob.a(rand)),
ob.ev(p, x, ob.b(rand)) ) |
the evaluation of the two parts of rand made
the parts of a combination |
| other |
ob.ap(ob.ev(p, x, rator),
ob.ev(p, x, rand) ) |
the evaluation of the rator applied to the
evaluation of the rand |
2.1.5 ob.ev Definition
ob.ev(p, x, phi)
= if is-individual(phi)
then oEvInt(p, x,
phi)
else if is-singleton(phi)
then ob.a(phi)
else oEvForm(p, x,
ob.a(phi), ob.b(phi))
The intended interpretation of ob.ev is as a function that assigns
to any
Ob phi as a formula the evaluation of that formula as an Ob. The arguments p and x are the
applicative
context of the evaluation.
2.1.6 oEvInt Definition
Every individual Ob has an eval interpretation. This interpretation
is the evaluation of the Ob as a formula or formal expression. The
intended interpretation is based on the same principle as for oApInt, except
there are only a few well-defined individuals that have any evaluation
interpretation other than themselves.
2.1.6.1 oEvInt(ob-SELF).
oEvInt(p, x, ob-SELF)
= p
2.1.6.2 oEvInt(ob-ARG).
oEvInt(p, x, ob-ARG)
= x
2.1.6.3 oEvInt(other).
oEvInt(p, x, other) = other,
for those other individuals introduced so far.
There will probably be other non-trivial oEvInt
3.1 Completeness and Universality from a Computational Perspective
Discussion of the idea of computational completeness over Ob and then provide
the demonstration of combinatory completeness (or applicative completeness,
which might be a better way to put it).
OK, the introduction of µ as a prefix doesn't really work
here. It is kind of like introducing a kind of O(f)
notation, which is a tempting idea but I don't want it in ‹ob›.
I think it works better to use µ as a relation symbol. This
will be a metalinguistic discussion, because the right hand side of µ
will be from a different theory! Also, I need a section to at least sketch
enough of Combinatory Algebra to have it be better motivated here. Many
Obs will be seen to realize various combinatory expressions, and so it is useful
to have that established to appeal to. I also have need to extend my use
of language like "the combinator that ap(cS, cK)
is." I had an insight about that this morning in the shower, so maybe
it will come back to me in the barber chair. All of this is to be gone
through in version 0.04 of the sketch. -- dh:2002-07-10]
3.2 Combinatory Algebra and Its Realization
We will demonstrate that the two combinators, cS and cK, are
representable in Ob. We use ob.ap as the interpretation of the combinatory
application operation, and then show two Obs that realize the combinators that cS and
cK are. [This is imprecise language and we have to straighten that
out. -- dh:2002-07-08]
The combinator cK is such that ap(ap(cK, cx),
cy)
is the combinator that cx is. [We need to say more about the
notational niceties being applied here. We are using typestyles and
prefixes and particular phrasings to remind ourselves that we are operating in
the combinatory theory, Ct, even though it is not laid out, just being
appealed to, for now. I am keeping such expressions distinct from those
about ‹ob›. This will be sorted out as I first make
the demonstration and then explore more-direct ways of explaining what is
happening. -- dh:2002-07-09]
The combinator cS is such that
ap(ap(ap(cS, cx), cy), cz)
is the combinator that ap(ap(cx, cz), ap(cy,
cz)) is.
Note that combinators are not Obs. The function ap(cc1,
cc2)
is a function on combinators that yields combinators.
For the demonstration of universality, we will show that there is a
realization of combinatory algebra in ‹ob›.
We take as the interpretation of ap, the Ob function ob.ap.
The realizations of combinators are not necessarily unique Obs. We
will say that a combinator, cc, has a realization in ‹ob›
if there is some Ob, a µcc, which is a realization of the combinator that
cc
is, and
For combinators cc, cd,
ob.ap(µcc, µcd)
is a realization of the combinator that ap(cc, cd)
is:
ob.ap( µcc, µcd)
is a µap(cc, cd).
Since all combinators in combinatory algebra can be expressed as applicative
expressions involving only the combinators cS and cK, our work is
done if we can show that there are Obs that are µcS and µcK.
3.3 Realizing cK
For a µcK, use ob-E.
ob.ap(ob.ap(ob-E, µcx), µcx
= ob.ap(ob.e(µcx), µcy)
= µcx
So the definition of cK is realized. Any µcx
(an Ob) is preserved intact, so that realization of combinator cx
is preserved, whatever combinator cx is. Likewise, the intermediate form
ob.ap(ob-E,
µcx) = ob.e(µcx)
realizes the combinator that ap(cK, cx) is.
That is, ob.e(µcx) is a µap(cK, cx).
3.4 Realizing cS
I have an existing solution,
from Miser 0.xx, that is much better because it uses some intermediate Obs and
allows this to be done in more direct pieces. Also, the intermediate Obs
are useful idioms for common situations in writing "programs" for ob.ap
and formulae for ob.ev. This will be done in version 0.04. --
dh:2002-07-10
We will work through the problem backwards to see how these realizations
are done, and to make the problem manageable:
3.4.1 For a µcS we require that
ob.ap(ob.ap(ob.ap(µcS, µcx), µcy), µcz)
= ob.ap(ob.ap(µcx, µcz),
ob.ap(µcy, µcz))
and that ob.ap(ob.ap( µcS, µcx), µcy)
is a µap(ap(cS, cx), cy).
3.4.2 For a µap(ap(cS, cx), cy)
use ob.c( ob.c(ob.e(µcx),
ob-ARG),
ob.c(ob.e(µcy), ob-ARG)
).
Then, in that case,
ob.ap(µ ap(ap(cS, cx), cy), µcz)
= ob.ap( ob.c( ob.c(ob.e( µcx),
ob-ARG),
ob.c(ob.e( µcy), ob-ARG)
),
µcz)
= oEvForm(µ ap(ap(cS, cx), cy), µcz,
ob.c(ob.e( µcx), ob-ARG),
ob.c(ob.e( µcy), ob-ARG)
)
= ob.ap(ob.ev(µ ap(ap(cS, cx),
cy), µcz,
ob.c(ob.e( µcx), ob-ARG),
ob.ev( µ ap(ap(cS, cx), cy), µcz,
ob.c(ob.e( µcy), ob-ARG)
)
= ob.ap(oEvForm(µ ap(ap(cS, cx),
cy), µcz,
ob.e(µcx),
ob-ARG),
oEvForm( µ ap(ap(cS, cx), cy), µcz,
ob.e( µcy),
ob-ARG)
)
= ob.ap(ob.ap(ob.ev(µ ap(ap(cS, cx),
cy), µcz,
ob.e( µcx) ),
ob.ev( µ ap(ap(cS, cx), cy), µcz,
ob-ARG)
),
ob.ap(ob.ev(µap(ap(cS, cx), cy), µcz,
ob.e( µcy) ),
ob.ev(µap(ap(cS, cx), cy), µcz,
ob-ARG)
)
)
= ob.ap(ob.ap(µcx, µcz),
ob.ap(µcy, µcz) ).
which is a µap(ap(cx, cz), ap(cy,
cz)) and a µap(ap(ap(cS, cx), cy), cz)
[We can maybe make this not so laborious if we demonstrate the expansion
through oEvForm as examples back in the definitions of ob.ap and ob.ev,
in section 2,. On the other hand, we only need to go through these
details to demonstrate this particular case, and we will streamline this kind
of development in later applications.-- dh:2002-07-09]
3.4.3 For a µap(cS, cx)
use ob.c( ob-C,
ob.c( ob.e(ob.c(ob.e(µcx),
ob-ARG)),
ob.c(ob-C,
ob.c( ob.c(ob-E,
ob-ARG),
ob.e(ob-ARG)
)
) )
).
Then, in that case,
ob.ap(µap(cS, cx), µcy)
= ob.ap( ob.c( ob-C,
ob.c( ob.e(ob.c(ob.e( µcx),
ob-ARG)),
ob.c(ob-C,
ob.c( ob.c(ob-E,
ob-ARG),
ob.e(ob-ARG)
)
) )
),
µcy)
= oEvForm(µap(cS, cx), µcy,
ob-C,
ob.c( ob.e(ob.c(ob.e( µcx),
ob-ARG)),
ob.c(ob-C,
ob.c( ob.c(ob-E,
ob-ARG),
ob.e(ob-ARG)
)
) )
)
= ob.c(ob.ev(µap(cS, cx), µcy,
ob.e(ob.c(ob.e( µcx),
ob-ARG)),
ob.ev(µap(cS, cx), µcy,
ob.c(ob-C,
ob.c( ob.c(ob-E,
ob-ARG),
ob.e(ob-ARG)
) )
)
)
= ob.c(ob.c(ob.e( µcx),
ob-ARG),
oEvForm(µap(cS, cx), µcy,
ob-C,
ob.c( ob.c(ob-E,
ob-ARG),
ob.e(ob-ARG)
)
)
)
= ob.c(ob.c(ob.e( µcx),
ob-ARG),
ob.c(ob.ev(µap(cS, cx), µcy,
ob.c(ob-E,
ob-ARG)
),
ob.ev(µap(cS, cx), µcy,
ob.e(ob-ARG)
)
)
= ob.c(ob.c(ob.e( µcx),
ob-ARG),
ob.c(oEvForm(µap(cS, cx), µcy,
ob-E,
ob-ARG
),
ob-ARG)
)
= ob.c(ob.c(ob.e( µcx),
ob-ARG),
ob.c(ob.ap(ob.ev(µap(cS, cx), µcy,
ob-E),
ob.ev(µap(cS, cx), µcy,
ob-ARG)
),
ob-ARG)
)
= ob.c(ob.c(ob.e( µcx),
ob-ARG),
ob.c(ob.ap(ob-E,
µcy
),
ob-ARG)
)
= ob.c(ob.c(ob.e( µcx),
ob-ARG),
ob.c(ob.e( µcy), ob-ARG)
)
which is a µ ap(ap(cS, cx), cy).
3.4.4 For µcS
[OK, One More to Go. This was easier the
last time I did it. I need to figure out how I cut it back and kept it
manageable. -- dh:2002-07-09]
The limitations of operating with Ob manifestations because there is no
externally/humanly-meaningful function. We can represent everything, but
communicate almost nothing. We don't even have the formalism of ‹ob›
theory available. We just have raw access to the manifestation of ‹ob›,
not the formalism (or metalanguage) in which we have been expressing Obs.
The idea of persistent description of Obs. That will be later. We
can "write" Obs in XML and we can "write" Obs in the
scripting language, Frugal.
More than that, there is the use of the Applicative Interpretation model,
and its extensions, to connect to the world in extremely useful, some might
say meaningful, ways.
Building-out and bridging will happen in this progression.
First, we will develop [o]Frugal, a scripting language that allows us to
express oMiser computations in something that is shareable among people and
that provides an external language that we can use to quickly manifest an ‹ob›
and exercise it in breadboard/prototype mode.
We will also develop obXML, a format in XML for expressing an [o]Miser Ob
such that it can be exchanged and then (re-) manifest on the same or different
computers at later times. The idea of manifestation elsewhere and
re-manifestation will provide interesting considerations.
With oMiser, there is no identified way, internal to ‹ob›,
to deal with symbols. So there is no way to deliver symbols to oMiser
and create computations that work with those symbols and incorporate symbols
in the result. This impairs our ability, using ‹ob› itself, to
provide formal manipulations (still on Obs) and that allow us to have Obs be
convenient expressions for forms that are tied to the intended purpose of
having our computations be interpretations of other important theories:
arithmetic, logic, and applications that arise in the purposive use of
computation. The inputs and results are still Obs, but we have a form of
individuals that makes Obs useful as symbolic expressions that are tied
to the purpose of an oMiser computation. This takes us to the sMiser level.
This is done by establishing a family of individual obs that provide an
external-world identity, expressed as a spelled symbol.
sMiser is accompanied by [s]Frugal, a scripting language that allows us to
take advantage of symbols (for people) in commanding Miser computations and
operating in the enriched sMiser world. (An [o]Frugal version exists
merely as a prototype fixture for exercising oMiser and obtaining obXML as a
way to save and restore our early work.)
sMiser is a baby step toward the development of iMiser, an
interactive/imperative system. It deals with important considerations of
language, identity, and the use of symbols that are not normally separated
out. We have a world without symbols, then we extend oMiser with symbols
that allow an interesting external sense of identity. We have not
actually done anything, but the result is far more convenient.
We now discuss the fact that every individual has an applicative
interpretation. Now, in oMiser, the application of any Ob to an Ob,
produces an Ob. This would appear to not be very fruitful.
Consider that an individual Ob can be the ‹ob› manifestation of
an object in some other system than ‹ob›. We cannot see,
directly in the ‹ob› manifestations, what these other
manifestations are. But whatever they accomplish, if we have a complete
primitive set of operations on them, also provided via Ob manifestations, we
know that we can create every computable function on those objects
using the already-established computational completeness of oMiser for
computations on Obs.
This is a giant leap, and better motivational examples will be
needed. It also helps to have Frugal-ese and sMiser to appeal to.
Which new kinds of theories do we manifest this way? Well, for
starters, the ones that let us express sFrugal and obXML processing in ‹ob›
itself.
-
- [McCarthy1960]
- Find the C.ACM Paper on theory for computation and the introduction of
S-Expressions, LISP, etc. It is now on-line as part of McCarthy's
papers.
-
- [More1979]
- More, Trenchard. Various technical reports and conference papers.
Find his use of individuals and singletons and
construct a reference for it. It should be in the APL 79 proceedings
and in IBM research papers before that. Iverson may have incorporated
that into something by now, too. [I still have a file folder on Array
Theory. Look there.]
- [Proskurowski1980]
- Proskurowski, Andrzej. On the Generation of Binary Trees. J.
ACM 27, 1 (January 1980), 1-2. [Tear sheet in file on
sorting]
- [Quine1969]
- Quine, Willard Van Orman. Set Theory and Its Logic.
Revised edition. Harvard University Press (Cambridge, MA: 1963,
1969). ISBN 0-674-80207-1 pbk. Readings
in Logic
Capture the quote about classes
and individuation not involving separation, extraction, or anything else
like that.
- [Rosenbloom1950]
- Rosenbloom, Paul C. The Elements of Mathematical Logic.
Dover (New York: 1950).
My expression of combinatory algebra is based on
that given in Rosenbloom's Chapter 3 section on combinatory logics.
- [Russell-PlatoQuote]
- Russell, Bertrand. On Knowledge and Perception in Plato. Now
where the heck did he say that.
- [Solomon1980]
- Solomon, Marvin., Finkel, Raphael A. A Note on Enumerating Binary
Trees. J. ACM 27, 1 (January 1980), 3-5. [Tear
sheet in file on sorting]
- [Strachey-McG]
- Strachey, Christopher. The McG Paper on macro generation, British
Computer Journal. Find that puppy again.
- [Wittgenstein ...]
- of course
-
- version 0.03 2002-07-10 (orcmid)
- This is recreated version 0.03, not like the original one, but
capturing what I had in mind for it, and more. The main goal is to
complete section 1. The expansion of sections 2 and 3 has led me
to freeze this version, because I now see where rework is
required. It is time to begin version 0.04 as an overhaul and also
look at reorganization for what is now a pretty long document. I
was getting where I felt I was losing my grip on the demonstration of
combinatory completeness in ‹ob›, and then found an old
1980-12-15 note of mine where I had worked it out and that still works,
though my explanation of what's happening is now along different lines,
using the manifestation metaphor which is new for me (whew).
- version 0.02 2002-07-03 (orcmid)
- Complete the first round on identity and start filling in later
sections with placeholders and basic notes, but not developed beyond
giving some statements of my intentions. This version is broken
off after a crash leaves me having to recreate changes here. This
provokes my providing more-careful attention to preserving history and
archiving of versions even though this is still a crude progression
before the sketch is ready for daylight. I also want to make it
available for early review and discussion with associates.
- version 0.01 2002-06-21 (orcmid)
- Start building the basic sketch so that people who are familiar with this kind of
system can get a sense of it until I stitch more in here and build out the
notes that have already been identified/started. There will also be
additional notes to support the sketch.
created 2002-06-16-18:31 -0700 (pdt) by orcmid
$$Author: Orcmid $
$$Date: 02-07-10 11:19 $
$$Revision: 32 $
Home