Self-reference is used to denote any situation in which someone or something refers to itself. A recent conference [PhiLog2002] is devoted to the issue of self-reference in philosophy, mathematics and computer science. The announcement of that conference triggered my thinking about this.
The theoretical foundation for Miser, the mathematical structure ob, exhibits self-reference in a variety of ways. There are two cases which are quite benign and not problematic in any apparent way.
However, one can use the universal computational function of Miser to represent self-referential situations that are problematical. We will identify and explore a particular example, after first disposing of those which, up to that point, appear completely benign.
The set Ob consists of elements that correspond to binary trees
Ob is denumerable
There are no cycles from leaves to other nodes in any Ob
The set of all functions on Ob, Of, consists of well-defined functions
The individuals, singletons, and composites are differentiated by whether and how they are immediately self-referential
This form of self-reference is benign
It supports ob being a floating theory in which Ob is closed with respect to the primitive functions and the primitive functions are total.
The manifestation of ob in a computer system uses computer storage and addresses in a straightforward way and the use of self-reference (that is, self-addressing stored values) raises no difficulties.
There is not even a problem with garbage collection and other techniques
The ob-ARG and ob-SELF individuals act as special constants that refer to other Obs determined in the context of evaluation of an Ob as a program (expression) for a computational procedure.
There is nothing about these constants that has there be anything explicitly self-referential
The operations pose no difficulty
The individuals are constants
The individuals are interpreted as context-relative references through the defined behavior of the ob.oEval function.
The presentation of ob.ap cases that constitute self-referential interpretations
We want these cases, they afford recursive definition and lambda-definability representations
In manifesting other kinds of elements, we get into trouble
The illustration of predicative sets
An easy way to introduce self-reference is with regard to predicative sets. That is, we will represent sets of Obs by functions that report whether or not a given Ob is a member of the set or not.
There is no particular difficulty with simple finite sets of Obs. The null set is simply
set-null(x) = no
and the "universal" set is represented via
set-Ob(x) = yes
A set of a single element would be something like
set-singleton(y) x = if x = y then yes else no
A set of several distinct Obs can be realized by
set-listing(L) x = is-member(x) L
where rec is-member(x) L
... as defined already below.
The important thing here is that the sets are being realized by the functions set-null, set-Ob, set-singleton(y), set-listing(L), etc.
And at the Miser level, we don't have the functions, but their programs, and these programs are themselves Obs.
So long as we use programs for sets, then we have the following operations on such "sets,"
set-complement(A) x = if A(x) then no else yes;
set-union(A, B) x = if A(x) then yes else B(x);
set-intersection(A, B) x = if A(x) then B(x) else no;
and so on.
This is a deficient characterization. What is missing is any way to distinguish and identify sets.
The need for symbols for certain forms of expression
Relationship to binding for Contextual References
Use in identification of self and args in the currying of Obs read as (symbolic) applicative expressions
The relationship to human interpretation and the appeal to external contexts -- self-reference as a meta-consideration
The oMiser system is devoid of symbols in any recognizable sense. The accomplishment of reference, to the extent there is any, is that embodied in the ob.ev rules, namely in the companion function, oEvInt.
At the same time, we very much want to have something like symbols, elements that serve as free variables (and can be bound) and in particular that can be used in recursive definitions.
This would permit oFugal expressions like
\closure \lambda.y \lambda.A \rec.is-member-y
'( (A = \b A) (\no :
(y = \a A)
(\yes : is-member-y \b A) ) )an optimization of the standard member function,
rec is-member(y) A
= if A = ob.b A
then no
else if y = ob.a A
then yes else is-member(y) ob.b A;In the normal approach in computer science, we need some construction that is usable as tags in oMiser. This is strictly a human convenience. That is, we want these to be uninterpreted symbols can be used in representation of symbolic expressions that are manipulated by Miser programs and that have some semblance to human-language symbolic expressions so that we can recognize what it is we are having be manipulated.
We can do this without having the tags denote anything, in much the way we have
ob.procnot denote anything, in a denotational sense, but we can just have these all be fixed elements that are useful as markers.Once we have tags, we can define ob.rec and ob.lambda by programs.
That is, we can have functions on Obs with the intended interpretation of the domain being applicative expressions (relative to ob.ap or ob.ev) and the tags are construed as free variables in those expressions. Then these functions can "bind" those free variables and in effect eliminate them.
The problem that tags give us is that any applicative interpretation (oApInt) for a tag can be an intended interpretation. We want these to "really be" uninterpreted symbols. This is not possible, even if we make oApInt of a tag be undefined. It could then be used for that.
There is more to think about here, in terms of what constitutes an uninterpreted symbol for oMiser, and what its nature is in ob. This conversations needs to be taken to a separate note. --dh:2002-10-26
Look at the standard self-reference situations and how they might have computational manifestations in Miser Systems.
The Liar: This Sentence is False
Russell's Paradox: Is the set of all sets that are not members of themselves an element of itself
Knower's Paradox: I know that what I say now is not true
"Actually, any theory that could be considered to be part of its own subject matter has some degree of self-referentiality. This applies to many theories of language, economy, sociology, psychology, etc. With respect to these theories an understanding of self-reference is essential to avoid performing unsound self-referential reasoning as in the paradoxes above." - From the [Philog2002] conference aims
See paradoxes, logical in The Oxford Companion to Philosophy.
See Mendelson's Introduction to Mathematical Logic for a run-down of logical paradoxes including Grelling's.
And see Principia Mathematica (p.60) for a rundown of the fundamental ones as considered by Whitehead and Russell.
There is then the question of self-referential sentences in the Gödel sense. This is a bigger deal and we need to look at what we can say about that here.
It appears that, in this context, a function does not refer to its own Gödel number.
The function or statement doesn't have a Gödel number.
In the context of ob, programs are their own Gödel numbers.
That these programs may realize functions on Obs is a different matter. The functions don't have Gödel numbers. Some expressions about them do.
It is not evident, at this point, whether honoring this point has any material impact on the arguments around halting and certainly not on the existence of non-computable functions in Of.
But it does, perhaps, make things more clear that this can be viewed as a conversation about representation.
- [PhiLog2002]
- The Danish Network for Philosophical Logic and Its Applications (PhiLog). Self Reference Conference. The Carlsberg Academy, Copenhagen. October 31 - November 2, 2002. http://www.philog.ruc.dk/phiconf2.html. [archive]
- Version 0.00: Initial Draft (orcmid)
- Outline the basic situation and what it implies for self-reference in ob and oMiser/oFrugal.
created 2002-10-25-13:53 -0700 (pdt) by orcmid
$$Author: Orcmid $
$$Date: 04-01-06 13:03 $
$$Revision: 5 $