Hostname: page-component-74656f9884-rdgjk Total loading time: 0 Render date: 2026-11-08T17:07:31.933Z Has data issue: false hasContentIssue false

Non-strict don't care algebras and specifications†

Published online by Cambridge University Press:  04 March 2009

Egidio Astesiano
Affiliation:
Dipartimento di Informatica e Scienze dell’Informazione, Via Dodecaneso 35, 16146 Genova (Italy) Email {astes, cerioli}@disi.unige.it
Maura Cerioli
Affiliation:
Dipartimento di Informatica e Scienze dell’Informazione, Via Dodecaneso 35, 16146 Genova (Italy) Email {astes, cerioli}@disi.unige.it

Abstract

Non-strict don't care functions, whose foremost representative is the ubiquitous if_then_else, play an essential role in computer science. As far as the semantics is concerned, they can be modelled by their totalizations with the appropriate use of elements representing undefinedness, as D. Scott has shown in his denotational approach. The situation is not so straightforward when we consider non-strict functions in the context of an algebraic framework; this point is discussed in the last section, where we explore the relationship between non-strict don't care and total algebras. The central part of this paper, after presenting the basic properties of the category of non-strict algebras, is an investigation of conditional algebraic specifications. It is shown that non-strict conditional specifications are equivalent to disjunctive specifications, and necessary and sufficient conditions for the existence of initial models are given. Since non-strict don't care specifications generalize both the total and the partial case, it is shown how the results for initiality can be obtained as specializations.

Information

Type
Research Article
Copyright
Copyright © Cambridge University Press 1996

Access options

Get access to the full version of this content by using one of the access options below. (Log in options will check for institutional or personal access. Content may require purchase if you do not have access.)

Article purchase

Temporarily unavailable