Kurt Gödel Research Center

2010 seminar talk: A Constructive Theory of Objects

Talk held by Masahiko Sato (Kyoto) at the KGRC seminar on 2010-03-18.

Abstract

A Constructive Theory of Objects
Masahiko Sato
Graduate School of Informatics, Kyoto University

We present a constructive theory of objects in which a Turing complete functional programming language, named Z, can be formally specified. Our theory is developed in two stages. 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 in which 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-like in 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.

We propose a new principle which we call the fundamental principle of object creation. Both symbolic expressions and symbolic objects are created inductively by following the fundamental principle. In this way, we see that the set of symbolic objects provides a natural framework for developing a constructive theory of objects, which contain both data objects and programs.