Re-grouping information in a domain-theoretic data model

In recent years, the problem of incorporating a set-building type-constructor into a domain theoretic data model has been addressed by different authors. In Jung and Puhlmann (1995) and Puhlmann (1995) we have shown why the so-called snack powerdomain is particularly suitable for modelling a set constructor. We obtain a generalized database model that covers the nested relational model.While, with the snack powerconstruction, the data structure of domain theoretic databases seems clear, suitable operations for the data model are still to be defined.In this paper we start this task by defining the operations nest and unnest for the passage between different nesting-levels of the snack powerconstruction. These functions are shown to form an embedding-projection pair, a property that the corresponding functions of nested relational databases do not have. This demonstrates the usefulness of the domain-theoretic approach for modelling databases: for the first time we have operators for re-grouping nested data that respect the idea of an information ordering.The use of the snack powerdomain leads to fairly complex formulas. To help the reader, illustrations and pictorial interpretations of formulas are given throughout the paper.

HYBRID PARTIAL-TOTAL TYPE THEORY

In this paper a hybrid type theory HTT is defined which combines the programming language notion of partial type and the logical notion of total type into a single theory. A new partial type constructor [Formula: see text] is added to the type theory: objects in [Formula: see text] may diverge, but if they converge, they must be members of the type A. A fixed point typing rule is given to allow for typing of fixed points. The underlying theory is based on ideas from Martin-Löf’s Intuitionistic Type Theory and Feferman’s Class Theory. The extraction paradigm of constructive type theory is extended to allow direct extraction of arbitrary fixed points. Important features of general programming logics such as LCF are preserved, including the typing of all partial recursive functions, a partial ordering [Formula: see text] on computations, and a fixed point induction principle. The resulting theory is thus intended as a general-purpose programming logic. Rules are presented and soundness of the theory established.

Trust in the lambda-calculus

This paper introduces trust analysis for higher-order languages. Trust<br />analysis encourages the programmer to make explicit the trustworthiness of<br />data, and in return it can guarantee that no mistakes with respect to trust will<br />be made at run-time. We present a confluent lambda-calculus with explicit trust<br />operations, and we equip it with a trust-type system which has the subject<br />reduction property. Trust information in presented as two annotations of each<br />function type constructor, and type inference is computable in O(n^3) time.

Parametric algebraic specifications with Gentzen formulas – from quasi-freeness to free functor semantics

Inspired by the work of S. Kaplan on positive/negative conditional rewriting, we investigate initial semantics for algebraic specifications with Gentzen formulas. Since the standard initial approach is limited to conditional equations (i.e. positive Horn formulas), the notion of semi-initial and quasi-initial algebras is introduced, and it is shown that all specifications with (positive) Gentzen formulas admit quasi-initial models.The whole approach is generalized to the parametric case where quasi-initiality generalizes to quasi-freeness. Since quasi-free objects need not be isomorphic, the persistency requirement is added to obtain a unique semantics for many interesting practical examples. Unique persistent quasi-free semantics can be described as a free construction if the homomorphisms of the parameter category are suitably restricted. Furthermore, it turns out that unique persistent quasi-free semantics applies especially to specifications where the Gentzen formulas can be interpreted as hierarchical positive/negative conditional equations. The data type constructor of finite function spaces is used as an example that does not admit a correct initial semantics, but does admit a correct unique persistent quasi-initial semantics. The example demonstrates that the concepts introduced in this paper might be of some importance in practical applications.

An Imperative Type Hierarchy with Partial Products

A <em>type hierarchy</em> for an imperative language defines an ordering on the types such that any application for small types may be reused for all larger types. The imperative facet makes this non-trivial; the straight-forward definitions will yield an inconsistent system. We introduce a new type constructor, the <em>partial product</em>, and show how to define a <em>consistent</em> hierarchy in the context of <em>fully recursive</em> types. A simple <em>polymorphism</em> is derived. By extending the types to include <em>stuctural invariants</em> we obtain a particularly appropriate notation for defining recursive types, that is superior to traditional type sums and products. We show how the ordering on types <em>extends</em> to an ordering on types with invariants. We allow the use of <em>least upper bounds</em> in type definitions and show how to resolve type equations involving these, and how to compute upper bounds of invariants.