ASMs and operational algorithmic completeness of lambda calculus

DOI10.1007/978-3-642-15025-8_16MaRDI QIDQ3586009zbMATHOpenAlexFDO

Authors Serge Grigorieff, Marie C. Ferbus-Zanda

Publication date 3 September 2010

Published in Fields of Logic and Computation (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1010.2597

zbMATH Keywords

lambda calculusASMoperational semanticstheory of algorithms

Mathematics Subject Classification ID

Combinatory logic and lambda calculus (03B40)

Abstract: We show that lambda calculus is a computation model which can step by step simulate any sequential deterministic algorithm for any computable function over integers or words or any datatype. More formally, given an algorithm above a family of computable functions (taken as primitive tools, i.e., kind of oracle functions for the algorithm), for every constant K big enough, each computation step of the algorithm can be simulated by exactly K successive reductions in a natural extension of lambda calculus with constants for functions in the above considered family. The proof is based on a fixed point technique in lambda calculus and on Gurevich sequential Thesis which allows to identify sequential deterministic algorithms with Abstract State Machines. This extends to algorithms for partial computable functions in such a way that finite computations ending with exceptions are associated to finite reductions leading to terms with a particular very simple feature.

Recommendations

• The transformation calculus
• scientific article; zbMATH DE number 7340317
• The weak lambda calculus as a reasonable machine
• scientific article; zbMATH DE number 783760
• An Introduction to the Lambda Calculus

Cites work

• scientific article; zbMATH DE number 1696772 (Why is no real title available?)
• scientific article; zbMATH DE number 1343482 (Why is no real title available?)
• scientific article; zbMATH DE number 1052006 (Why is no real title available?)
• scientific article; zbMATH DE number 783760 (Why is no real title available?)
• A Natural Axiomatization of Computability and Proof of Church's Thesis
• A call-by-name lambda-calculus machine
• Abstract State Machines
• Combinatory logic. With two sections by William Craig.
• Efficient self-interpretation in lambda calculus
• Evolving Algebras 1993: Lipari Guide
• One-tape, off-line Turing machine computations
• Palindrome recognition using a multidimensional tape.
• Processes, Terms and Cycles: Steps on the Road to Infinity
• Sequential abstract-state machines capture sequential algorithms
• The lambda calculus. Its syntax and semantics. Rev. ed.
• The parametric lambda calculus. A metamodel for computation.

Cited in

(2)

• The transformation calculus
• Axiomatization and characterization of BSP algorithms

This page was built for publication: ASMs and operational algorithmic completeness of lambda calculus

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3586009)