Well-definedness, semantic type-checking, and type inference for database query languages

The well-definedness problem for a programming language consists of checking, given an expression and an input type, whether the semantics of the expression is defined for all inputs adhering to the input type. A related problem is the semantic type-checking problem which consists of checking, given an expression, an input type, and an output type whether the expression always returns outputs adhering to the output type on inputs adhering to the input type. Both problems are undecidable for general-purpose programming languages. In this dissertation we study those problems for specific-purpose database query languages. We show that they remain undecidable in general. We identify potential sources of this undecidability and propose corresponding restrictions that ensure decidability.; Next, we study classical type system problems from the theory of programming languages in the context of database query languages. Given an expression in the language, without type declarations for the input variables, there is the problem of whether there are any input type declarations under which the expression is well-typed. Moreover, if there are, then which are they, and what is the corresponding output type for each of these? We study these problems for the relational algebra and the named nested relational calculus.