Universal algebras with lazy and partial functions

Olov Wilander

(University of Uppsala)

It is well known that equational logic is not sound for structures
with partial functions. A sound system for Horn logic with partial
functions, called PHL (investigated by E. Palmgren and S. Vickers), is
one of many alternative systems. In this talk, we simplify and extend
PHL to handle, not only partial, but also lazy functions.

The system is given semantics in a way that stays very close to the
traditional universal algebra semantics for equational logic, and both
soundness and completeness is shown. Further, some proof theoretic
properties of the new system, particularly regarding the substitution and
cut rules, are investigated. Finally its precise relation to PHL is
clarified by means of intertranslatability results.

Tuesday 19th June 2007, 14:00
Robert Recorde Room
Department of Computer Science