Giuseppe Della Penna ; Benedetto Intrigila ; Giulio Manzonetto - Addressing Machines as models of lambda-calculus

lmcs:7645 - Logical Methods in Computer Science, July 29, 2022, Volume 18, Issue 3 -
Addressing Machines as models of lambda-calculusArticle

Authors: Giuseppe Della Penna ; Benedetto Intrigila ; Giulio Manzonetto

    Turing machines and register machines have been used for decades in theoretical computer science as abstract models of computation. Also the $\lambda$-calculus has played a central role in this domain as it allows to focus on the notion of functional computation, based on the substitution mechanism, while abstracting away from implementation details. The present article starts from the observation that the equivalence between these formalisms is based on the Church-Turing Thesis rather than an actual encoding of $\lambda$-terms into Turing (or register) machines. The reason is that these machines are not well-suited for modelling $\lambda$-calculus programs. We study a class of abstract machines that we call "addressing machine" since they are only able to manipulate memory addresses of other machines. The operations performed by these machines are very elementary: load an address in a register, apply a machine to another one via their addresses, and call the address of another machine. We endow addressing machines with an operational semantics based on leftmost reduction and study their behaviour. The set of addresses of these machines can be easily turned into a combinatory algebra. In order to obtain a model of the full untyped $\lambda$-calculus, we need to introduce a rule that bares similarities with the $\omega$-rule and the rule $\zeta_\beta$ from combinatory logic.

    Volume: Volume 18, Issue 3
    Published on: July 29, 2022
    Accepted on: May 13, 2022
    Submitted on: July 2, 2021
    Keywords: Computer Science - Logic in Computer Science

    Consultation statistics

    This page has been seen 1384 times.
    This article's PDF has been downloaded 487 times.