A computation model for executable higher-order algebraic specification languages

Jean Pierre Jouannaud, Mitsuhiro Okada

Research output: Chapter in Book/Report/Conference proceedingConference contribution

80 Citations (Scopus)

Abstract

The combination of (polymorphically) typed lambda-calculi with first-order as well as higher-order rewrite rules is considered. The need of such a combination for exploiting the benefits of algebraically defined data types within functional programming is demonstrated. A general modularity result, which allows as particular cases primitive recursive functionals of higher types, transfinite recursion of higher types, and inheritance for all types, is proved. The class of languages considered is first defined, and it is shown how to reduce the Church-Rosser and termination (also called strong normalization) properties of an algebraic functional language to a so-called principal lemma whose proof depends on the property to be proved and on the language considered. The proof of the principal lemma is then sketched for various languages. The results allows higher order rules defining the higher-order constants by a certain generalization of primitive recursion. A prototype of such primitive recursive definitions is provided by the definition of the map function for lists.

Original languageEnglish
Title of host publicationProceedings - Symposium on Logic in Computer Science
PublisherPubl by IEEE
Pages350-361
Number of pages12
ISBN (Print)081862230X
Publication statusPublished - 1991 Jul
Externally publishedYes
EventProceedings of the 6th Annual IEEE Symposium on Logic in Computer Science - Amsterdam, Neth
Duration: 1991 Jul 151991 Jul 18

Other

OtherProceedings of the 6th Annual IEEE Symposium on Logic in Computer Science
CityAmsterdam, Neth
Period91/7/1591/7/18

Fingerprint

Functional programming
Religious buildings
Specification languages

ASJC Scopus subject areas

  • Engineering(all)

Cite this

Jouannaud, J. P., & Okada, M. (1991). A computation model for executable higher-order algebraic specification languages. In Proceedings - Symposium on Logic in Computer Science (pp. 350-361). Publ by IEEE.

A computation model for executable higher-order algebraic specification languages. / Jouannaud, Jean Pierre; Okada, Mitsuhiro.

Proceedings - Symposium on Logic in Computer Science. Publ by IEEE, 1991. p. 350-361.

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Jouannaud, JP & Okada, M 1991, A computation model for executable higher-order algebraic specification languages. in Proceedings - Symposium on Logic in Computer Science. Publ by IEEE, pp. 350-361, Proceedings of the 6th Annual IEEE Symposium on Logic in Computer Science, Amsterdam, Neth, 91/7/15.
Jouannaud JP, Okada M. A computation model for executable higher-order algebraic specification languages. In Proceedings - Symposium on Logic in Computer Science. Publ by IEEE. 1991. p. 350-361
Jouannaud, Jean Pierre ; Okada, Mitsuhiro. / A computation model for executable higher-order algebraic specification languages. Proceedings - Symposium on Logic in Computer Science. Publ by IEEE, 1991. pp. 350-361
@inproceedings{d3bb24edabb34833b294be4f51df9f52,
title = "A computation model for executable higher-order algebraic specification languages",
abstract = "The combination of (polymorphically) typed lambda-calculi with first-order as well as higher-order rewrite rules is considered. The need of such a combination for exploiting the benefits of algebraically defined data types within functional programming is demonstrated. A general modularity result, which allows as particular cases primitive recursive functionals of higher types, transfinite recursion of higher types, and inheritance for all types, is proved. The class of languages considered is first defined, and it is shown how to reduce the Church-Rosser and termination (also called strong normalization) properties of an algebraic functional language to a so-called principal lemma whose proof depends on the property to be proved and on the language considered. The proof of the principal lemma is then sketched for various languages. The results allows higher order rules defining the higher-order constants by a certain generalization of primitive recursion. A prototype of such primitive recursive definitions is provided by the definition of the map function for lists.",
author = "Jouannaud, {Jean Pierre} and Mitsuhiro Okada",
year = "1991",
month = "7",
language = "English",
isbn = "081862230X",
pages = "350--361",
booktitle = "Proceedings - Symposium on Logic in Computer Science",
publisher = "Publ by IEEE",

}

TY - GEN

T1 - A computation model for executable higher-order algebraic specification languages

AU - Jouannaud, Jean Pierre

AU - Okada, Mitsuhiro

PY - 1991/7

Y1 - 1991/7

N2 - The combination of (polymorphically) typed lambda-calculi with first-order as well as higher-order rewrite rules is considered. The need of such a combination for exploiting the benefits of algebraically defined data types within functional programming is demonstrated. A general modularity result, which allows as particular cases primitive recursive functionals of higher types, transfinite recursion of higher types, and inheritance for all types, is proved. The class of languages considered is first defined, and it is shown how to reduce the Church-Rosser and termination (also called strong normalization) properties of an algebraic functional language to a so-called principal lemma whose proof depends on the property to be proved and on the language considered. The proof of the principal lemma is then sketched for various languages. The results allows higher order rules defining the higher-order constants by a certain generalization of primitive recursion. A prototype of such primitive recursive definitions is provided by the definition of the map function for lists.

AB - The combination of (polymorphically) typed lambda-calculi with first-order as well as higher-order rewrite rules is considered. The need of such a combination for exploiting the benefits of algebraically defined data types within functional programming is demonstrated. A general modularity result, which allows as particular cases primitive recursive functionals of higher types, transfinite recursion of higher types, and inheritance for all types, is proved. The class of languages considered is first defined, and it is shown how to reduce the Church-Rosser and termination (also called strong normalization) properties of an algebraic functional language to a so-called principal lemma whose proof depends on the property to be proved and on the language considered. The proof of the principal lemma is then sketched for various languages. The results allows higher order rules defining the higher-order constants by a certain generalization of primitive recursion. A prototype of such primitive recursive definitions is provided by the definition of the map function for lists.

UR - http://www.scopus.com/inward/record.url?scp=0026190438&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=0026190438&partnerID=8YFLogxK

M3 - Conference contribution

AN - SCOPUS:0026190438

SN - 081862230X

SP - 350

EP - 361

BT - Proceedings - Symposium on Logic in Computer Science

PB - Publ by IEEE

ER -