Program Calculation Properties of Continuous Algebras

M.M. Fokkinga, Erik Meijer

Research output: Book/ReportReport

Abstract

Defining data types as initial algebras, or dually as final co-algebras, is beneficial, if not indispensible, for an algebraic calculus for program construction, in view of the nice equational properties that then become available. It is not hard to render finite lists as an initial algebra and, dually, infinite lists as a final co-algebra. However, this would mean that there are two distinct data types for lists, and then a program that is applicable to both finite and infinite lists is not possible, and arbitrary recursive definitions are not allowed. We prove the existence of algebras that are both initial in one category of algebras and final in the closely related category of co-algebras, and for which arbitrary (continuous) fixed point definitions ("recursion") do have a solution. Thus there is a single data type that comprises both the finite and the infinite lists. The price to be paid, however, is that partiality (of functions and values) is unavoidable. We derive, for any such data type, various laws that are useful for an algebraic calculus of programs.
LanguageUndefined
Place of PublicationAmsterdam, The Netherlands
PublisherCentrum voor Wiskunde en Informatica
Number of pages47
StatePublished - Jan 1991

Publication series

NameReport / Department of Computer Science
PublisherCWI
No.CS-R91

Keywords

  • IR-66626
  • EWI-8201

Cite this

Fokkinga, M. M., & Meijer, E. (1991). Program Calculation Properties of Continuous Algebras. (Report / Department of Computer Science; No. CS-R91). Amsterdam, The Netherlands: Centrum voor Wiskunde en Informatica.
Fokkinga, M.M. ; Meijer, Erik. / Program Calculation Properties of Continuous Algebras. Amsterdam, The Netherlands : Centrum voor Wiskunde en Informatica, 1991. 47 p. (Report / Department of Computer Science; CS-R91).
@book{ef62438271c247c584a6cd7af81282ac,
title = "Program Calculation Properties of Continuous Algebras",
abstract = "Defining data types as initial algebras, or dually as final co-algebras, is beneficial, if not indispensible, for an algebraic calculus for program construction, in view of the nice equational properties that then become available. It is not hard to render finite lists as an initial algebra and, dually, infinite lists as a final co-algebra. However, this would mean that there are two distinct data types for lists, and then a program that is applicable to both finite and infinite lists is not possible, and arbitrary recursive definitions are not allowed. We prove the existence of algebras that are both initial in one category of algebras and final in the closely related category of co-algebras, and for which arbitrary (continuous) fixed point definitions ({"}recursion{"}) do have a solution. Thus there is a single data type that comprises both the finite and the infinite lists. The price to be paid, however, is that partiality (of functions and values) is unavoidable. We derive, for any such data type, various laws that are useful for an algebraic calculus of programs.",
keywords = "IR-66626, EWI-8201",
author = "M.M. Fokkinga and Erik Meijer",
note = "Imported from EWI/DB PMS [db-utwente:tech:0000003528]",
year = "1991",
month = "1",
language = "Undefined",
series = "Report / Department of Computer Science",
publisher = "Centrum voor Wiskunde en Informatica",
number = "CS-R91",
address = "Netherlands",

}

Fokkinga, MM & Meijer, E 1991, Program Calculation Properties of Continuous Algebras. Report / Department of Computer Science, no. CS-R91, Centrum voor Wiskunde en Informatica, Amsterdam, The Netherlands.

Program Calculation Properties of Continuous Algebras. / Fokkinga, M.M.; Meijer, Erik.

Amsterdam, The Netherlands : Centrum voor Wiskunde en Informatica, 1991. 47 p. (Report / Department of Computer Science; No. CS-R91).

Research output: Book/ReportReport

TY - BOOK

T1 - Program Calculation Properties of Continuous Algebras

AU - Fokkinga,M.M.

AU - Meijer,Erik

N1 - Imported from EWI/DB PMS [db-utwente:tech:0000003528]

PY - 1991/1

Y1 - 1991/1

N2 - Defining data types as initial algebras, or dually as final co-algebras, is beneficial, if not indispensible, for an algebraic calculus for program construction, in view of the nice equational properties that then become available. It is not hard to render finite lists as an initial algebra and, dually, infinite lists as a final co-algebra. However, this would mean that there are two distinct data types for lists, and then a program that is applicable to both finite and infinite lists is not possible, and arbitrary recursive definitions are not allowed. We prove the existence of algebras that are both initial in one category of algebras and final in the closely related category of co-algebras, and for which arbitrary (continuous) fixed point definitions ("recursion") do have a solution. Thus there is a single data type that comprises both the finite and the infinite lists. The price to be paid, however, is that partiality (of functions and values) is unavoidable. We derive, for any such data type, various laws that are useful for an algebraic calculus of programs.

AB - Defining data types as initial algebras, or dually as final co-algebras, is beneficial, if not indispensible, for an algebraic calculus for program construction, in view of the nice equational properties that then become available. It is not hard to render finite lists as an initial algebra and, dually, infinite lists as a final co-algebra. However, this would mean that there are two distinct data types for lists, and then a program that is applicable to both finite and infinite lists is not possible, and arbitrary recursive definitions are not allowed. We prove the existence of algebras that are both initial in one category of algebras and final in the closely related category of co-algebras, and for which arbitrary (continuous) fixed point definitions ("recursion") do have a solution. Thus there is a single data type that comprises both the finite and the infinite lists. The price to be paid, however, is that partiality (of functions and values) is unavoidable. We derive, for any such data type, various laws that are useful for an algebraic calculus of programs.

KW - IR-66626

KW - EWI-8201

M3 - Report

T3 - Report / Department of Computer Science

BT - Program Calculation Properties of Continuous Algebras

PB - Centrum voor Wiskunde en Informatica

CY - Amsterdam, The Netherlands

ER -

Fokkinga MM, Meijer E. Program Calculation Properties of Continuous Algebras. Amsterdam, The Netherlands: Centrum voor Wiskunde en Informatica, 1991. 47 p. (Report / Department of Computer Science; CS-R91).