Word operation definable in the typed \(\lambda\)-calculus
type: Item
instance of: scholarly article
title: Word operation definable in the typed \(\lambda\)-calculus
zbMATH Open document ID: 0638.03014
DOI: 10.1016/0304-3975(87)90077-6
author: Marek Zaionc
published in: Theoretical Computer Science
publication date: 1987-01-01T00:00:00Z
review text: The problem of representability of word functions over a binary (any finite) alphabet by closed terms of the type \(\underline B^ n\to \underline B\) (where \(\underline B = (0\to 0)\to ((0\to 0)\to (0\to 0)))\) is solved. It is proved that the set FUN Ḇ, i.e. \(\cup^{\infty}_{i=1}Cl(\underline B^ i\to \underline B),\) is finitely generated. This is an extension of Schwichtenberg's and Statman's results.
Mathematics Subject Classification ID: 03B40
Mathematics Subject Classification ID: 03D05
Mathematics Subject Classification ID: 68Q45
zbMATH DE Number: 4039852
zbMATH Keywords: typed lambda calculus
zbMATH Keywords: lambda-definability
zbMATH Keywords: representability of word functions
reviewed by: Pavel Materna
MaRDI profile type: Publication
full work available at URL: 0304-3975(87)90077-6
OpenAlex ID: W2090288940
cites work: The lambda calculus, its syntax and semantics
cites work: Q5565113
cites work: Q4068706
cites work: A unification algorithm for typed \(\overline\lambda\)-calculus
cites work: Axiom schemes for m-valued propositions calculi
cites work: Definierbare Funktionen imλ-Kalkül mit Typen
cites work: The typed lambda-calculus is not elementary recursive
cites work: On the existence of closed terms in the typed lambda calculus II: Transformations of unification problems
cites work: λ-definable functionals andβη conversion
cites work: Q3708774
cites work: Q4124327
description: scientific article; zbMATH DE number 4039852