A lattice theoretic approach to computation based on a calculus of partially ordered type structures (property inheritance, semantic nets, graph unification)
Hassan Aı̈t-Kaci · Scholarly Commons (University of Pennsylvania) · 1984
The purpose of this thesis is twofold: (1) to define a formal lattice-theoretic calculus of partially ordered type structures where the ordering is meant to reflect subtyping; (2) to propose a model of computation which amounts to solving systems of simultaneous equations in a lattice of types. The specific contributions which I believe to be original of the research presented here are: (1) An extrapolation of the syntactic properties of first-order terms to provide insight in formalizing record-like type structures; (2) A simple "type-as-set" semantics and a motivational discussion of what this entails for the operational use of partially ordered types in programming; (3) A lattice-theoretic calculus of type subsumption and a formal universal construction extending this calculus in the light of the foregoing discussion; (4) An efficient algorithm to compute greatest lower bounds of type structures; (5) The definition of a particular language (KBL) based on solving recursive equations in the lattice of types, and a fixed-point semantics study of its model of computation.