Algebra of constructions. I. The word problem for partial algebras
type: Item
instance of: scholarly article
title: Algebra of constructions. I. The word problem for partial algebras
zbMATH Open document ID: 0653.03010
DOI: 10.1016/0890-5401(87)90018-6
author: Adam Obtułowicz
published in: Information and Computation
publication date: 1987-01-01T00:00:00Z
review text: The paper presents an algebraic approach to abstract computing systems based on the lambda-calculus and cartesian closed categories. First, axioms of cartesian closed categories are formalized using the language of partial equational logic. Then, constructions of certain categories from words are presented, where partial operations are computable functions. A general formulation of the word problem for a theory in partial equational logic is provided, and the notions of a normal system and an algebra of constructions are defined. Decidability of the word problem for cartesian closed categories is proven in a new way, based on a construction of a normal system which is a recursive partial algebra as a free model of the theory of cartesian closed categories.
Mathematics Subject Classification ID: 03B40
Mathematics Subject Classification ID: 18D15
Mathematics Subject Classification ID: 68Q65
Mathematics Subject Classification ID: 08A50
Mathematics Subject Classification ID: 08A55
zbMATH DE Number: 4064958
zbMATH Keywords: algebraic approach to abstract computing systems
zbMATH Keywords: lambda-calculus
zbMATH Keywords: cartesian closed categories
zbMATH Keywords: partial equational logic
zbMATH Keywords: word problem
zbMATH Keywords: normal system
zbMATH Keywords: algebra of constructions
zbMATH Keywords: recursive partial algebra
reviewed by: Jiří Zlatuška
MaRDI profile type: Publication
full work available at URL: 0890-5401(87)90018-6
OpenAlex ID: W2081822152
cites work: The lambda calculus. Its syntax and semantics. Rev. ed.
cites work: Q3785893
cites work: Q5612462
cites work: Q5343326
cites work: Functional completeness of cartesian categories
cites work: Q3727946
cites work: Q4769119
cites work: Q5639839
cites work: Constructive mathematics and computer programming
cites work: Q4726252
cites work: Q3659756
cites work: Locally cartesian closed categories and type theory
cites work: Combinators, \(\lambda\)-terms and proof theory
cites work: Algebra of proofs
cites work: Q5609363
description: scientific article; zbMATH DE number 4064958