A Free Construction of Dynamic Terms

摘要

In this paper we show that it is possible to extend in a natural way to the dynamic case some basic results of the classical approach to (static) data types. Within an appropriate framework of dynamic structures (calledd-oids), which play the same role as algebras in the static case, we define a language of dynamic terms, also enjoying the property of unique canonical representation; moreover, dynamic terms constitute a free structure whenever the static terms in the underlying static framework are so. As a main application of the above construction, we get a rather elegant kernel language for recursive definitions of dynamic derived operations, which parallels the well-known McCarthy's schema for a kernel applicative language. This kernel language can be seen also as a metalanguage for expressing the semantics of concrete (e.g., imperative or object-based) languages.