Assigning Meanings to Symbolic Objects– A Constructive Theory of Objects –Masahiko Sato
Graduate School of Informatics
Kyoto Universitymasahiko@kuis.kyoto-u.ac.jp

Abstractor, by the equation:

We present a constructive theory of objects in which a
Turing complete functional programming language, namedZ, can be formally specified. Our theory is developed in twostages. In the first stage, we introduce a set of symbolic expressions generated from two initial objects by two binary
operators. This set is used as the meta-level universe inwhich the object language defined in the second stage is interpreted. In the second stage, we define the syntax of Z, by
inductively defining a set of symbolic objects. Z is Lisp-likein the sense that both data and programs of Z are symbolic
objects. We give both operational and denotational semantics to Z by interpreting Z data and programs as symbolic
expressions.

1. Introduction
The purpose of this paper is (1) to present a simple theory of symbolic expressions by defining the class hSexpri
of symbolic expressions, (2) to develop a theory of symbolic objects by defining the class hObjecti of symbolic objects, and (3) to define a functional programming language
Z by assigning meanings to symbolic objects. Both operational and denotational semantics will be given to Z byusing hSexpri as the semantic domain to interpret the Z programs, i.e., symbolic objects.
All members of hSexpri and hObjecti are created following the principle which we call the fundamental principle ofobject creation:
Every object o is created from already created nobjects o1 , . . . , on (n ≥ 0) by applying a creation
method M .
We can visualize this act of creation by the following figure:
o1

···
o

on

M

o = M (o1 , . . . , on )As these visualizations suggest, we consider the method M
as a rule and also as a function. Here, we require that eachcreation method must satisfy the freeness conditions, thatis, (1) the method must be injective, and (2) objects createdby the method must be disjoint from objects created by anyother method. The first condition is a local condition which
depends only on the method while the second condition isa global condition which depends on all creation methods
available for creating objects.
If we create objects following the fundamental principle
augmented by the freeness conditions, then we can uniquely
recover M , n and o1 , . . . , on by analyzing the created object o. This fact implies that any object carries in itself acomplete history of how it is created. So, we define two objects to be equal if and only if they are created exactly in thesame way, and this equality makes our theory an intensional
one (§??). We can also attach the scheme of proof-byinduction based on our inductive creation of objects and use
it to prove that every object enjoys a certain property. Similarly, we can inductively define functions on objects, that is,
we can attach a value to an object o = M (o1 , . . . , on ) using
the values attached to oi .
Our fundamental principle is a natural generalization of
the principle that is used to define the set of natural numbers
inductively. However, as far as we know, the present workis the first systematic application of the principle to create
basic data structures (including functions and classes) thatare necessary to develop a constructive theory of objects.
In §??, we follow the fundamental principle to define
the class hSexpri of symbolic expressions by means of 4
creation methods Nil, T, Cons and Snoc. Here, the class
hSexpri is defined as the set of those objects that can be created by the 4 methods, and simultaneously, we define theconcept Sexpr (we use ‘Sexpr’ as an abbreviation of ‘symbolic expression’) by stipulating that an object o falls underthe concept Sexpr (or, o is an Sexpr) iff o is a member (or, an
instance) of the class hSexpri (which we write o : hSexpri).
Following Frege [?], we view a concept as a function which,when applied to an object, returns the judgement assertingthat the object falls under the concept. In this view, for example, we can write Sexpr(o) for the application of the concept Sexpr to an object o, and read it: o is an Sexpr.
In §??, we define the class hObjecti of symbolic objects,
as well as its subclasses necessary to define hObjecti. In
order to satisfy the freeness conditions, the construction isdone independently from the construction in §??. As in §??,
a class c is defined simultaneously with a concept C andthey are related by the property: for any symbolic objecto, o is a C iff o : c holds. We will say that c the associated class of C . The concepts introduced in this section
are selected so that they form a minimal collection of concepts necessary to make hObjecti a Turing complete programming language we define in §??.
In §??, we give operational and denotational semantics
of Z in the domain hSexpri. Our denotational semantics is
unique in that with each Z expression e we assign four denotations JeKp (denotation of e as a program), JeKd (as adatum), JeKf (as a function) and JeKc (as a class), where, depending on e some of these denotations may be undefined.
§?? gives concluding remarks comparing our work withrelated works. Philosophical motivation for this work is also
discussed there.

are infinite supply of tokens for each kind. We can implement these methods either by the rules:[] Nil

() T

s t
Snoc
(s|t)

or, equivalently, by the defining equations:
Nil() := [],T() := (),Cons(s, t) :=[s|t],
Snoc(s, t) :=(s|t).

In the creation methods Cons and Snoc above, s and t must
be Sexprs already created. It is easy to verify the freenessof these methods. We have thus completed the definitionsof the class hSexpri and the concept Sexpr. The class wedefined is categorical in the sense that any two algebraic
systems having the given signature and satisfying the freeness conditions are isomorphic. Thus ΣhSexpri specifies theclass abstractly but uniquely (up to isomorphism).
We write S for the class hSexpri when we view it as aconcrete set of token sequences we have just implemented,
and call it the universe of symbolic expressions. Thus S
becomes a concrete algebra having signature ΣhSexpri andsatisfying the domain equation:
S = Nil() + T() + Cons(S, S) + Snoc(S, S)
where all the 4 creating methods are injective. We will also
call these 4 methods constructors of Sexprs. In order toanalyze Sexprs constructed thus, we introduce recognizers
and selectors as follows.
We introduce the four recognizers:

2. Symbolic Expressions
In this section, we define the class hSexpri of symbolic
expressions by creating its members following the fundamental principle. The concept Sexpr is defined by sayingthat any member of hSexpri is an Sexpr. Now, we define theclass hSexpri by the signature:
Nil :

s t
Cons
[s|t]

Nil? : hSexpri → hSexpri
Cons? : hSexpri → hSexpri
T? : hSexpri → hSexpri
Snoc? : hSexpri → hSexpri→ hSexpri

where each recognizer returns () (true) if the given Sexpr iscreated by the method in question and [] (false) otherwise.
Following Lisp’s convention, we write t for () and nil
for []. For example, we have Cons?([t|nil]) = t andNil?(t) = nil.
As for selectors, we have:Cons : hSexpri hSexpri → hSexpri
T:→ hSexpri
Snoc : hSexpri hSexpri → hSexpri
where each of the creation methods Nil and T creates a
new Sexpr from zero already created Sexprs, and each of
the creation methods Cons and Snoc creates a new Sexpr
from two already created Sexprs. Have we really defined
the class hSexpri and the concept Sexpr? No! We have only
specified the signature of hSexpri, written ΣhSexpri . So, we
have to explicitly show the existence of 4 methods having
the signature ΣhSexpri and satisfying the freeness conditions(§??). We do this by implementing these methods as concrete methods of placing the 5 kinds of tokens ‘[’, ‘]’, ‘(’,‘)’ and ‘|’, from left to right, where we assume that there

Car : hSexpri 99K hSexpri
Cdr : hSexpri 99K hSexpri
Head : hSexpri 99K hSexpri
Tail : hSexpri 99K hSexpri

We used the dash arrow symbol ‘99K’ to indicate that thesefunctions are partial functions from hSexpri to hSexpri. The
selectors Car and Cdr are used to select Sexprs that are used
to create an Sexpr by the creation method Cons. That is,2

hObjecti

Car(s) (Cdr(s)) selects the first (second, respectively) Sexpr

hListihTupleithat is used to construct s and they are defined only when
Cons?(s) = t. Similarly, the selectors Head and Tail areused to select Sexprs from an Sexpr created by the Snoc
method. There are no selectors for nil and t since they
are created from zero previously created Sexprs.
We have thus introduced 12 functions (4 constructors,
4 recognizers and 4 selectors) on hSexpri. By adding themechanism of conditional computation and the mechanismof defining a new function by recursion we can define theclass of computable functions on hSexpri in an analogous
way as we define computable functions on natural numbers.
Let us introduce a form of conditional computation:

hpatterni
hsymbolihConstantihclass-namei
hfun-namei
hVariablei
hatomihClassihNati
hEnvi
hFunctionie[a; b; c; d]which is computed as follows. First, we compute e. If edoes not have a value, then the value of the form is undefined. If e has a value, then e’s value is either (1) nil, (2) aConsed object, (3) t, or (4) a Snoced object. We then compute a in case (1), b in case (2), c in case (3) and d in case(4). We call this form a case-form. We also introduce an
if-form eha; bi (read: if e then a else b) by putting:Figure 1. hObjecti and its subclasses
We conclude this section by introducing a number of notational conventions that we will use in the coming sections.
• [s] := [s|[]]• [s1 · · · sn ] := [s1 |[s2 · · · sn ]](n ≥ 2)eha; bi := e[b; a; a; a]
The value of this if-form is: the value of a if e has a nonnil value, the value of b if e has value nil, and undefinedotherwise.
As an example of a recursive definition of a function, we
define the function Eq? which decides for given two objects
whether they are equal:• (s) := (s|())• (s1 · · · sn ) := (s1 |(s2 · · · sn ))(n ≥ 2)
We also abbreviate [s|[t|u]] ((s|(t|u))) to [s t|u]((s t|u), respectively), etc.

Eq?(x, y) :=3. Symbolic Objects

x[yhnil; ti;y[nil; nil;
Eq?(Car(x), Car(y))hEq?(Cdr(x), Cdr(y)); nili;
nil];

In this section, we define the class hObjecti of symbolic
objects together with its 13 subclasses. Figure 1 shows the
subclass relation among these 14 classes. We call a classbasic class if it is the collection of all the objects which canbe created by one or more specified creation methods. Thusa basic class is defined by specifying its creation methods.
A non-basic class is called a derived class and it is definedeither as a union of two or more classes or as a subclassof another class. When we name a class, we follow theconvention of capitalizing the first letter of the name of abasic class and use lower-case letters for a derived class1 .
So, for example, hListi is a basic class and hsymboli is a
derived class.
As in §??, classes and concepts are defined in three steps:
specification, implementation and verification. However, tosave space, we skip the specification step here2 and directly

yht; nili;y[nil; nil; nil;Eq?(Head(x), Head(y))hEq?(Tail(x), Tail(y)); nili]]

We have the following theorem which shows that Eq?
computes the equality relation correctly.
Theorem 1. For any Sexprs s and t, we have Eq?(s, t) = t
if and only if s = t.
Proof. First we can show by the double induction on creations of s and t that Eq? is a total function and always
return either nil or t. Then, again by the double induction on creations of s and t, we can show that (1) if
Eq?(s, t) = t, then s = t and (2) if Eq?(s, t) = nil, thens 6= t.

1 An exception is the derived class hObjecti. We capitalize the initialletter since this class forms the universe of symbolic objects.
2 See Appendix ?? for the specification.

3

implement the specified classes as a set of sequences of thefive tokens we used in §??. The verification that our implementation satisfies the freeness conditions is easy and weremark on this only in §??. This implementation determines
the concrete syntax of our programming language Z.

Just as we could define all the computable functions on
hSexpri by the 12 primitive functions defined in §??, we
can define all the computable functions on hObjecti using
these 5 primitive functions and the 14 creation methods weintroduce in §??–§??.

3.1. Object

3.2. List

We define the class hObjecti as the union of 4 disjointclasses:

We define the class hListi as a basic class whose members are created by the methods:

hObjecti := hTuplei + hListi + hsymboli + hatomi[] : hListi

where hsymboli is defined as the union of 2 disjoint basic
classes (§??) and hatomi is defined as the union of 4 disjoint
basic classes (§??). Thus hObjecti becomes the union of 8
disjoint basic classes. We define the mother class of an Object as the unique basic class to which the Object belongs.
We write U for the class hObjecti when we view it as aconcrete set of token sequences, and call it the universe ofsymbolic objects. Actually, we implement hObjecti in sucha way that each Object as a token sequence belongs to theset S. Thus, we will have U ⊆ S. Note that this is an accidental fact that depends on our particular implementationof hSexpri and hObjecti. Hence, this fact does not meanthat hObjecti is a subclass of hSexpri. Rather, these twoclasses are conceptually independent, and we could implement these two classes so that they become mutually disjoint.
As we are following the fundamental principle, any Object o is created by its creation method from already createdObjects: o = M (o1 , . . . , on ). Here, we call M the creation
method of o, and oi (1 ≤ i ≤ n) the i-th component of o3 .
In order to be able to completely and uniformly analyze o,
we introduce the 5 primitive functions below:
method :
1st :
2nd :
3rd :

nil

a : hObjecti b : hListi
cons[a|b] : hListi

We have the following recognizers and selectors.
nil? : hObjecti → hObjecti
cons? : hObjecti → hObjecti
car :
cdr :

hListi 99K hObjecti
hListi 99K hListi

The recognizer cons?, for instance, is defined by:cons?(x) := =?(method(x), cons)

where cons is the function name (§??) for the function
cons. This recognizer decides if x is created by the creation method cons. We can similarly define the recognizer
M ? for every creation method M . Using these recognizers,
we can define the recognizer C ? for every class C . For
instance, the recognizer List? : hObjecti → hObjecti is defined by:
List?(x) := or(nil?(x), cons?(x))

where or decides if one of its arguments is (). The selector
car is defined by 1st but differs from 1st in that car is defined
only on hListi. For example, car of a Tuple (a|b) (§??) is
undefined (since a Tuple is not a List) while 1st returns a.
cdr is defined similarly.

hObjecti → hfun-namei
hObjecti 99K hObjecti
hObjecti 99K hObjecti
hObjecti 99K hObjecti=? : hObjecti hObjecti → hObjecti

3.3. Tuple

The function method computes the creation method M ofo. As M itself can never be an Object (a method is something the operates on Objects at meta-level) the function
method cannot directly return M , so it returns instead thename of the creation method M (see §??). The functions
1st, 2nd and 3rd respectively compute the first, second andthird component of o. Finally, =? is a binary function which
decides whether given two Objects are equal or not. Thus=? returns () (true) if they are equal, and [] (false) otherwise.

The class hTuplei is defined as a basic class whose structure is isomorphic to the structure of hListi. Although
hTuplei and hListi share the same mathematical structure,
it is useful to have both classes and distinguish them conceptually. In general, we will use Tuples to encode Cartesian products of several classes, and use Lists to encode sequences of the the same or similar classes.
The creation methods for hTuplei are:() : hTuplei

3 In our construction of hObjecti, n is at most 3.

4ta : hObjecti b : hTuplei
snoc(a|b) : hTuplei

3.8. Class

We have the following functions for tuples.
t? : hObjecti → hObjecti

A Constant is said to be a class-name if it is <Object>,<List>, . . . , or <Function>, namely, if it corresponds to

snoc? : hObjecti → hObjectia name of the 14 classes listed in Figure 1.
The class hClassi is a basic class and it has the creation
method class:head : hTuplei 99K hObjecti
tail : hTuplei 99K hTupleic : hclass-namei
class(c|<Class>) : hClassi

3.4. Symbol
The derived class hsymboli is defined as the union of two
disjoint basic classes hConstanti and hVariablei.

This method creates a Class which, in Z, internalizes the(meta-level) class whose class-name is c. So, we can define
the following function:

3.5. Constantin? : hObjecti hClassi → hObjecti

The basic class hConstanti is defined by the following
creation method:with the property: in?(o, (c|<Class>)) = t iff o : C ,where C is the meta-level class whose class-name is c.

o : hObjecti
constant[o|()] : hConstanti

3.9. Natural Number

We introduce a notational convention for expressing some Constants in typewriter font. For example, the convention allows us to write ab for the Constant [[(()()[][][][]())(()()[][][]()[])]|()].
Here, we used 7-bit ASCII code for encoding ASCII characters.

The class hNati is defined by the two creation methods:(zero|<Nat>) : hNati

zero(n|<Nat>) : hNati
succ((succ n)|<Nat>) : hNati

We use decimal notation to denote Nats. For instance, 0 =(zero|<Nat>) and 1 = ((succ zero)|<Nat>).
We have the following selector for natural numbers:

3.6. Variable
The basic class hVariablei is defined by:pred : hNati 99K hNatio : hObjecti
variable[o|(())] : hVariablei

which returns the predecessor of n for n 6= 0.

As a notational convention, we will write a Variable inslant typewriter font. For example, x denotes the Variable[(()()()()[][][])|(())].

3.10. Environment
We define the basic class hEnvi by the following two creation methods:

3.7. Atom([]|<Env>) : hEnvi

The class hatomi is defined as the union of 4 disjoint
basic classes:

empty

s : hsymboli v : hObjecti (E|<Env>) : hEnvi
put([(s v)|E]|<Env>) : hEnvi

hatomi := hClassi + hNati + hEnvi + hFunctioni

For the sake of notational convenience, we abbreviate([b1 · · · bn ]|<Env>) to {b1 · · · bn }, where each bi isa pair of a symbol and an Object. We also write E[v/s] forput(s, v, E).
An Env is global (local) if each si is a Constant (Variable, respectively). We use the meta-variables Γ and ∆ forglobal Envs and Λ and Π for local Envs. A pair of global
and local Envs is used to provide a context in which Constants and Variables are evaluated (§??).

Each subclass C of hatomi will be defined in such a waythat any Object o in C will be of the form (a|c) wherec is a Constant which is the class-name (§??) of C , anda is an Object which together with c enables us to recoverfrom o the components and the creation method of o. It thenfollows that all subclasses of hatomi are mutually disjoint
as well as that hatomi is disjoint from hListi, hTuplei andhsymboli.
5We define the following functions:

The creation method defun is defined by the rule:g : hConstanti p : hpatterni b : hTuplei
defun((f g p|b)|<Function>) : hFunctioni

get : hsymboli hEnvi 99K hObjecti
conc :

hEnvi hEnvi → hEnvi

This rule, as well as the next rule for defmacro, must satisfy
a special side condition on g. We explain the condition inCase 1.2 and Case 1.3 of §??. The Tuple b is the body ofthe defined Function. After the method is invoked, the valueof the Constant g becomes the Function created by defun(§??). So, the method defun not only creates a new Function
but also assigns the name g to the created function.
The creation method defmacro is defined by the rule:

The value of get(s, E) is defined only if E contains a Tupleof the form (s v), and in this case, get returns the v of theleftmost such Tuple. We will write E(s) for get(s, E). We
define the size of an Env E, written |E|, to be the numberof symbols s for which E(s) is defined. The function conc
concatenates two Envs in an obvious way. For instance, wehave conc({a b}, {c d}) = {a b c d}. We write E, E 0 forconc(E, E 0 ).

g : hConstanti p : hpatterni b : hTuplei
defmacro((m g p|b)|<Function>) : hFunctioni

3.11. PatternIn §??, we explain how we can dynamically extend theopen-ended universe hObjecti using defun and defmacro.

A Tuple d is said to be a declaration if it is of the form x,(c x) or of the form (&rest c x) where c is a class-name(§??) and x is a Variable. If d is of the third form, it is calleda special declaration. A pattern is defined to be a Tuple ofthe form (d1 · · · dn ) where each di is a declaration.
A pattern is used to match a Tuple against it. So we
define the binary partial function

4. Meanings of Symbolic Objects
In §?? we defined the universe of symbolic objects U asa subset of the universe of symbolic expressions S. In thissection we assign meanings to Objects by treating Objects
as Sexprs and by viewing them as programs, data, functions
and classes.
First we give a meaning of the Z language by viewing
each Object as a program. To this end, we define a binary evaluation relation e ⇓ v (read: e evaluates to v, ore has value v, or e denotes v) between two Objects e (which
we call a program) and v (which we call a value). To be
more precise, the evaluation of a program is done in a context determined by two Envs of which one is global and theother is local. So the evaluation relation depends on thesetwo Envs. Moreover, the context itself sometimes changes
after the evaluation since our language supports dynamic
extension of the universe by Function definitions.Thus, ingeneral, an evaluation relation is not a binary relation but arelation on 6 Objects, which we write:

match : hTuplei hpatterni 99K hEnvi

which matches a Tuple e against a pattern p, and returns an Env if the matching succeeds. For the patternp = ((<List> x) (<Nat> y)), for instance, we havematch(([] 1), p) = {(x []) (y 1)}. On the other
hand, match((() 1), p) is undefined since () is not ahlisti. But we have match((()), (x)) = {(x ())}
since the declaration x is treated as an abbreviation of(<Object> x). Just as in Lisp, a special declaration isused to bind a Tuple of Objects to a single Variable, but weskip the details.

3.12. Function
The class hFunctioni is a basic class and it has the creation methods function, defun and defmacro.

Γ; Λ ` e ⇓ v a ∆; Πc : hfun-namei
function(c|<Function>) : hFunctioni

where Γ; Λ is the context before the evaluation and ∆; Π isthe context after the evaluation. However, we will continue
to express the relation as a binary relation leaving Envs implicit. Or, we will write Γ ` e ⇓ v a ∆ (Λ ` e ⇓ v a Π)
when we can leave local (global, resp.) Envs implicit. We
define the relation e ⇓ v inductively on how e is created.
A List is evaluated by the two rules below:

In this method, c must be a fun-name (function name), thatis, it must be one of the following Constants:
set! defun defmacro progn let if quotemethod 1st 2nd 3rd =? cons snoc
constant variable class zero succ
empty put function[] ⇓ []

The first 7 fun-names in the above list create macro Functions and the remaining 14 fun-names create call-by-value
Functions.

a⇓u b⇓v[a|b] ⇓ [u|v]

In order to guarantee the deterministic evaluation (Theorem??), we understand that the premises of each evaluation rule6

where g must be a Constant whose value is undefined in Γ.
Note that when g satisfies this side-condition, we can invoke
the (meta-level) method defun and can extend the universe
U dynamically by adding a new Function to the universe.
1.3 The rule for f = (defmacro|<Function>) is:are evaluated from left to right. Thus the second rule above,
written in full, is:Γ; Λ ` a ⇓ u a Γ0 ; Λ0 Γ0 ; Λ0 ` b ⇓ v a Γ00 ; Λ00
Γ; Λ ` [a|b] ⇓ [u|v] a Γ00 ; Λ00
A symbol is evaluated by retrieving its value from thecurrent global or local Env. The value is undefined if thevalue is not found in the Env.
c : hConstanti Γ(c) = v
Γ ` c⇓v a Γg : hConstanti p : hpatterni b : hTupleiΓ ` (g p|b) 7→f () a Γ[((m g p|b)|<Function>)/g]

x : hVariablei Λ(x) = v
Λ ` x⇓v a Λ

where g must be a Constant whose value is undefined in Γ.
1.4 The rules for f = (progn|<Function>) are:e : hatomie⇓e

In the second rule, b must be a non-() Tuple. The Function
progn evaluates members of its argument one by one andreturn the value of the last member.
1.5 To define the rule for f = (let|<Function>), we
introduce an auxiliary binary relation Π ⇓Env Π0 on local
Envs as follows.

From Figure 1, we see that the only remaining case to becovered by the evaluation rules is the case where the program to be evaluated is a Tuple. To cover this case, it isnecessary to introduce an auxiliary ternary relation e 7→f v(read: the result of applying f to its argument e is v, or f
maps e to v) among a Function f , a Tuple e and an Object
v. This relation also depends on contexts which we leave
implicit as much as possible. Using this application relation, we can define the following two evaluation rules for a
Tuple:f ⇓g() ⇓ ()

g : hFunctioni(f |e) ⇓ v

a ⇓ u b 7→f v(a|b) 7→f v

a⇓v(a) 7→f v

An atom evaluates to itself.

Π : hEnvia1 ⇓ v1 · · ·Π ⇓Env Π0an ⇓ vn

where Π = {(x1 a1 ) · · · (xn an )}.
and Π0{(x1 v1 ) · · · (xn vn )} (n ≥ 0).
Using this relation, we give the rule for f(let|<Function>) as follows.

e 7→g v==Λ ` Π ⇓Env Π0 a Λ0 Π0 , Λ0 ` e 7→g v a Π00 , Λ00Λ ` (Π|e) 7→f v a Λ00

The first rule is for evaluating (). The second is for evaluating a Tuple which is not (). This rule says that (f |e)
has value v if and only if f evaluates to a Function g andthe result of applying g to e is v.
The application relation e 7→f v is defined by case analysis (case 1 to case 4 below) on the creation of Functionf.
Case 1: In this case we give evaluation rules for theprimitive call-by-name Functions we introduced in §??.
The first 3 functions (1.1–1.3) are used to change the surrounding contexts and the values returned by these functions are less significant.
1.1 The rules for f = (set!|<Function>) are:where g = (progn|<Function>) and Λ0 (Π0 ) and Λ00(Π00 , resp.) must be of the same length. Here, Π is used
to create a temporarily extended local Env Π0 , Λ0 , and the
body e of the let-form is evaluated in the extended local
Env. The extended part of the Env is thrown away after theevaluation.
1.6 The rules for f = (if|<Function>) are:c ⇓ () a ⇓ v(c a b) 7→f v

c ⇓ [] b ⇓ v(c a b) 7→f v

1.7 The rule for f = (quote|<Function>) is:c : hConstanti Γ ` a ⇓ v a ∆ x : hVariablei Λ ` a ⇓ v a ΠΓ ` (c a) 7→f v a ∆[v/c]Λ ` (x a) 7→f v a Π[v/x](e) 7→f e

In the left rule above, c must be a Constant which does nothave a value in ∆. In the right rule above, on the other hand,x must be a Variable which does have a value in Π. We have|∆| = |Γ| + 1 and |Π| = |Λ| when these rules are applied.
1.2 The rule for f = (defun|<Function>) is:

Case 2: We now give rules for call-by-value primitive
Functions. In call-by-value Function application, a Function’s argument is evaluated before application. To define
the rule for this case, we introduce two auxiliary binary relations. The first one is e ⇓Tup v on Tuples defined as follows.

g : hConstanti p : hpatterni b : hTupleiΓ ` (g p|b) 7→f () a Γ[((f g p|b)|<Function>)/g]

e1 ⇓ v1 · · · en ⇓ vn(n ≥ 0)(e1 · · · en ) ⇓Tup (v1 · · · vn )7

The second relation e Bf v is a ternary relation among a
Function f , Tuple e and Object v. The relation is defined asfollows.
f (v1 , . . . , vn ) = v(n ≥ 0)(v1 . . . vn ) Bf v

(defmacro tuple (&rest a)(if (t? a) a
(snoc snoc
(snoc (head a)(snoc (snoc tuple (tail a)) t))))))(defmacro while (c &rest b)(tuple if c(tuple progn (snoc progn b)(snoc while (snoc c b)))nil))(defun + ((<nat> m) (<nat> n))(if (=? n 0) m (succ (+ m (pred n)))))(defun * ((<nat> m) (<nat> n))(if (=? n 0) 0 (+ (* m (pred n)) m)))(defun factr ((<nat> n))(if (=? n 0) 1 (* n (factr (pred n)))))(defun facti ((<nat> n))(let {(result 1)}(while (not (=? n 0))(set! result (* n result))(set! n (pred n)))result))where f is the meta-level function that corresponds to f
whose computation rule we gave in §??. For example, if
f is (car|<Function>), then f is car defined in §??.
Now, the general rule for such a Function f is:e ⇓Tup u u Bf v
e 7→f v
Case 3 f = ((f g p|b)|<Function>): This is thecase where f is defined by the defun method.
Λ ` e ⇓Tup u a Λ0match(u, p) = ΠΠ ` b 7→h v a Π0

Λ ` e 7→f v a Λ0
where h = (progn|<Function>). Here, the argument e
is evaluated as a Tuple in the surrounding local Env Λ, andthe result is used to create a local Env Π. Then, the body bof f is evaluated in Π.
Case 4 f = ((m g p|b)|<Function>): This is thecase where f is defined by the defmacro method. In thiscase f is intended to work as a macro (in the sense of Lisp).
match(e, p) = ΠΠ ` b 7→h b0 a Π0
Λ ` e 7→f v a Λ0

Figure 2. Example of Function Definitions
addition (+) and multiplication (*) on hNati, the factorial
Function is defined by recursion (factr) and by iteration(facti). All of these Functions were tested on a prototype
Z interpreter which we implemented in Emacs Lisp. The
evaluation relation enjoys the following properties.

Λ ` b0 ⇓ v a Λ0

where h = (prog|<Function>). Here, the body b of f
is evaluated in the temporal local Env Π, and the result b0 isevaluated in the surrounding local Env Λ.

Theorem 2. If Γ; Λ ` e ⇓ v a ∆; Π and Γ; Λ ` e ⇓ v 0 a∆0 ; Π0 , then v = v 0 , ∆ = ∆0 , Π = Π0 , |Γ| ≤ |∆| and|Λ| = |Π|.

We have thus completed the definition of the evaluation
relation. We now give a few examples of evaluation in Z.
If the global Env is Γ0 = {} in which no Constant has avalue, what would be the first program we wish to evaluate?
Our recommendation is:

Corollary 1. If Γ; {} ` e ⇓ v a ∆; Π, then Π = {}.
Theorem ?? shows that evaluation is deterministic.
Corollary ?? characterizes the top-level of a Z interpreter.
Namely, the interpreter sets the local Env to be empty before the evaluation of a program, and only the global Env Γ
might change to ∆ after the evaluation either by the set!
command on a Constant, by the defun command, or by
the defmacro command. The interpreter then evaluates
the next program input by the user in the new global Env ∆.
We can see this cycle of evaluation as a process of dynamically changing the universe U of symbolic objects. To
analyze this process, we take advantage of the fact that wehave implemented U as a subset of S. So, we will work in
S and see how U can be extended within S. We say thata global Env ∆ is realizable if either (1) ∆ = {} or (2)∆ = Γ[o/c], where Γ is realizable, c is a Constant, and ∆is obtained by applying a function f in Case 1.1–1.3. So,a realizable Env can actually be obtained by evaluating Z
programs appropriately. It is easy to see that we can decide,
for any Sexpr, if it is a realizable Env.

((set!|<Function>) set! (set!|<Function>))By evaluating this program, the Constant set! is set tohave the function s = (set!|<Function>) as its value,
and we get a new Env Γ1 in which we have set! ⇓ s . Soin Γ1 (and afterwards) we can use set! as a shorthand fors , and both (set! x a) and (s x a) have the samevalue (if any) for any a. We can continue to set values
for Constants as we like in this way. In particular, we set
quote to (quote|<Function>) and, as in Lisp, write ’efor (quote e). We also set values to Constants which correspond to primitive functions and classes as well as [] tonil and () to t.
Having done this, we can extend our universe bydefmacro and defun as shown in Figure 2. There, wefirst define the macro Function while. Then, after defining
8Let Γ be a realizable Env. We say that a Function f is a
Γ-defined Function if f = Γ(g) for some Constant g. We
define UΓ to be the smallest subset X of S such that (1) X
contains all the Γ-defined Functions and (2) X is closed under all the creation methods other than defun and defmacro.
It is easy to see that UΓ is a decidable subset of S. We define
the partial function:

application of our principle to λ-calculus can be found in[?].
The development of our open-ended class hObjecti is influenced by Martin-Löf’s development of dependent typetheories (see, e.g., [?, ?]), but the crucial difference between
these developments is that we view any object as an instanceof its mother Class while Martin-Löf views any object as anelement of a type. We believe that, from a foundational
point of view, the notion of class is more basic than that oftype since, in our theory, a Class is always associated witha concept.
We have given a big-step operational semantics of thelanguage Z by defining an evaluation relation on Z Objects.
We already gave a big-step semantics of Hyperlisp in [?, ?],but here the rules are more elaborate since Z admits dynamic changes of both global and local Envs. We have also
given a denotational semantics of Z, by providing 4 different views of Z Objects.
Our theory of object is intensional since our universe
must be created following the fundamental principle withthe freeness conditions. By taking this view, however,equality of two Functions can be easily decided in Z. We
also remark that, at meta-level, we can view Z Functions
extensionally by taking the program-view. For example,
let Γ be the Env we obtained, in §??, after we defined
the two factorial Functions f and g where f (g) computes
the factorial by recursion (iteration, resp.). Then, we have
ΓJf Kp 6= ΓJgKp , but ΓJf Kf = ΓJgKf as a meta-level function on hNati. Our theory is natural since we cannot understand the contents of mathematics unless, first of all, weunderstand the syntax of the language in which mathematics
is written.
Z is a Lisp-like (see, e.g. [?]) language in the sense thatboth data and programs are represented by symbolic objects. The biggest difference between Z and Lisp is that every Z object belongs to its mother Class where the mother
Class itself is a Z object, but this is not the case in Lisp
since there are no built-in classes in Lisp (although there
are some extensions (e.g., CLOS [?]) of Lisp with classes
as objects. Moreover, each Z Class is created as an Z object by reifying (see Quine [?] for a philosophical accountof the concept of reification) the corresponding meta-levelclass listed in Figure 1. In fact, we first analyzed the primitive concepts that are necessary to realize a Turing complete
language from scratch, and obtained the data structure of Z
by reifying these primitive concepts. Therefore, Figure 1
can been seen as a concept map which shows a minimal
set of primitive concepts necessary to develop the notion ofcomputation.
The present work is a part of our long-term project ([?])
of creating a computer environment for supporting humanmathematical activity. Philosophical motivation for the
project is as follows. As a core subject of science, mathe-evalΓ : UΓ 99K S

by putting evalΓ (e) = v iff Γ; {} ` e ⇓ v a Γ0 ; {} forsome Γ0 . We also write ΓJeKp for evalΓ (e). ΓJeKp gives thedenotation (in S) of e viewed as a program.
Let us now turn to other views of Z Objects. We canview an Object o ∈ UΓ as a datum simply by viewing it
as o ∈ S. So, we define the denotation of o as a datum by
ΓJoKd := o. The datum-view and program-view are relatedby the equality: ΓJoKd = ΓJ’oKp , which holds for any o ∈UΓ .
The denotation of an Object as a function is given only
when it is a Function (§??). Given a realizable Env Γ and a
Function f ∈ UΓ , we can define a meta-level function:f : S 99K S
by putting f (x) = v iff Γ ` (x) 7→f v a Γ0 for some
Γ0 . (To simplify the argument, we assume that f is defined by defun with the pattern p = (x).) We write ΓJf Kf
for f and call it the denotation of f as a function. The
function-view and program-view are related by the equality:
ΓJf Kf (ΓJxKp ) ' ΓJ(f x)Kp which holds for any x ∈ UΓ ,where ‘'’ means that if one side of the equation has a definite value, the other side also has the same value.
The class-view is given only to a Z Class (§??). For
a Class C, its denotation as a class (written ΓJCKc ) is themeta-level class that corresponds to C. For example, wehave (<Class>|<Class>) ∈ hClassi. The class-view
and program-view are related by the equivalence: ΓJxKp ∈ΓJCKc ⇔ ΓJ(in? x C)Kp = () (x ∈ UΓ ).
In summary, among the four views, the program-view is
the most basic since the other three views can be characterized by the program-view as we have just seen.

5. Conclusions
We have developed a constructive theory of objects
based on the fundamental principle of object creation. The
fundamental principle we proposed in this paper is inspiredby a similar principle proposed by Conway [?] to developa theory of numbers and games. The difference is that wehave created our universe based on a constructive view ofobjects, while Conway created his universe based on a platonistic view without imposing the freeness conditions. An
9following equations:nil :cons :
t:snoc :
constant :variable :class :→ hListihObjecti hListi → hListi→ hTuplei
hObjecti hTuplei → hTuplei
hObjecti → hConstanti→ hNatihNati → hNati→ hEnvi

succ :
empty :
function :We specify the remaining derived classes hpatterni,hclass-namei and hfun-namei in terms of axioms for thecorresponding concepts pattern, class-name and fun-name.
First, we introduce constants c1, . . . , c14 for the 14 classnames together with the 15 axioms:

hObjecti → hVariableihclass-namei → hClassi

zero :

put :hObjecti := hListi + hTuplei + hsymboli + hatomi
hsymboli := hConstanti + hVariablei
hatomi := hNati + hEnvi + hFunctioni + hClassi

class-name(c1), . . . , class-name(c14)andConstant(x) ⇐ class-name(x)hsymboli hObjecti hEnvi → hEnvi
hfun-namei → hFunctioni

The first 14 axioms assert that each of the 14 constants is aclass-name, and the last axiom asserts that any class-name isa Constant. We can specify the concept fun-name similarly.
To specify the concept pattern, we introduce a constant r,
and we also specify the concept decl (declaration). In theaxioms for decl, we we write (c x) for snoc(c, snoc(x, t()))
and understand (r c x) similarly.

defun : hConstanti hpatterni hTuplei → hFunctioni
defmacro : hConstanti hpatterni hTuplei → hFunctioni

Figure 3. Signature of hObjecti

Constant(r) ⇐decl(x) ⇐ Variable(x)matics is not a completed collection of mathematical knowledge. Rather, our mathematical knowledge is dynamicallyextended, day by day, by our scientific activity. The extensibility, or the open-endedness, of mathematics comesfrom a key feature of mathematics: introduction of new concepts and objects by definitions. Thus it is essential for our
project to formalize and implement this key feature. Basedon this motivation, we have introduced a theory of objects
with the aim of supporting the key feature. The language Z,
as defined here, supports introduction of new functions, butdoes not support introduction of new concepts. We have aplan of adding this feature by incorporating a function, say
defclass, which enables us to add new classes to U dynamically. We are also hoping that, by the introduction ofthis feature, Z will become a class-based functional objectoriented programming language.

decl((c x)) ⇐ class-name(c), Variable(x)decl((r c x)) ⇐ class-name(c), Variable(x)pattern(t()) ⇐pattern(snoc(d, p)) ⇐ decl(d), pattern(p)References[1] H. Abelson and G. J. Sussman. Structure and Interpretationof Computer Programs, 2nd edition. The MIT Press, 1996.
[2] J. H. Conway. On Numbers and Games, 2nd edition. A K Peters Ltd., 2001.
[3] G. Frege. On Function and Concept. in The Frege Reader,
M. Beaney (ed.), Blackwell Publishing, 130–148, 1997.
[4] P. Martin-Löf. Intuitionistic Type Theory. Bibliopolis, Napoli,
1984.
[5] B. Nordström, K. Peterson and J. M. Smith. Programmingin Martin-Löf’s Type Theory – An Introduction –, Clarendon
Press, Oxford, 1990.
[6] M. Sato and M. Hagiya. Hyperlisp. Proceedings of the International Symposium on Algorithmic Language, 251–269,
North-Holland, 1981.
[7] M. Sato. Theory of symbolic expressions, I. Theoretical Computer Science, 22:19–55, 1983.
[8] M. Sato and R. Pollack. External and internal syntax of the
λ-calculus, Journal of Symbolic Computation, to appear.
[9] M. Sato. A framework for checking proofs naturally, Journalof Intelligent Information Systems, 31:111–125, 2008.
[10] S. Keene. Object-Oriented Programming in Common Lisp:
A Programmer’s Guide to CLOS, Addison-Wesley, 1988.
[11] W. V. O. Quine. From a Logical Point of View (2nd ed.,revised) Harvard University Press, Cambridge, MA, 1980.

A. Specification of hObjecti
We give the specification of the 14 classes listed in Figure 1. Of these classes 8 are basic classes and they are specified by the signature ΣhObjecti shown in Figure 3. For example, the second item says that cons is to be a method
which creates a new List from an object and an List. However, as we have seen in §??, in our implementation, themethods defun and defmacro may be applied only if theirfirst argument, a Constant, satifies a special side-condition.
The specification given here does not cover this point.
The 6 derived classes are specified as follows. The
classes hObjecti, hsymboli and hatomi are specified by the10