An algebraic semantics approach to the effective resolution of type equations (Q1093359)

This article presents a syntactic calculus of partially-ordered data type structures and its application to computation. A syntax of record-like terms and a type subsumption ordering are defined and shown to form a lattice structure. A simple `type-as-set' interpretation of these term structures extends this lattice to a distributive one, and in the case of finitary terms, to a complete Brouwerian lattice. As a result, a method for solving systems of type equations by iterated rewriting of type symbols is proposed which defines an operational semantics for KBL - a Knowledge Base Language. It is shown that a KBL program can be seen as a system of equations. Thanks to the lattice properties of finite structures, systems of simultaneous type equations are shown to admit least fixed-point solutions. An operational semantics for KBL is described as term rewriting. Fan-out rewriting, a particular rewriting computation order related to the conventional outermost term rewriting which rewrites symbols closer to the root first, is defined and shown to be maximal. Correctness with respect to least fixed-point semantics of KBL's operational semantics, as defined by fan-out rewriting, is discussed. Finally, extensions and further research directions are sketched.