Abstract Machines for Logic Programs(chrisistyping.bearblog.dev)
chrisistyping.bearblog.dev
Abstract Machines for Logic Programs
https://chrisistyping.bearblog.dev/abstract-machines-for-logic-programs/
4 comments
Thanks. I thought it was interesting choosing arithmetic instead of some other relation because multimodal arithmetic (via CLP) is more of a PhD thesis than a blog post. Other relations might've been easier to demonstrate a general query.
What I couldn't tell from the article was if the author somehow achieved a multimodal arithmetic relation without needing CLP using a stack machine. That would be a neat technique.
What I couldn't tell from the article was if the author somehow achieved a multimodal arithmetic relation without needing CLP using a stack machine. That would be a neat technique.
> I've recently been curious about the abstract machines implied by this process for other kinds of programs.
Olivier Danvy's "Rational Reconstruction of the SECD Machine" [0] explores the idea of this transformation as well, but frames it as a relationship between operational and denotational semantics:
> This deconstruction–reconstruction is actually interesting in itself because it provides a bridge between small-step operational semantics (in the form of an abstract machine) and denotational semantics (in the form of a compositional evaluation function)
His work on (de/re)functionalization is super interesting.
[0]: https://link.springer.com/chapter/10.1007/11431664_4
Olivier Danvy's "Rational Reconstruction of the SECD Machine" [0] explores the idea of this transformation as well, but frames it as a relationship between operational and denotational semantics:
> This deconstruction–reconstruction is actually interesting in itself because it provides a bridge between small-step operational semantics (in the form of an abstract machine) and denotational semantics (in the form of a compositional evaluation function)
His work on (de/re)functionalization is super interesting.
[0]: https://link.springer.com/chapter/10.1007/11431664_4
So if you're confused because of the slightly unusual notation, here's the same thing in Prolog syntax:
It doesn't work this way in general because the Prolog is/2 predicate can only be used in one direction to evaluate the term on the right hand side where must all variable must be bound to a number in context. The article mentions Peano arithmetic as one finite/incomplete axiomatisation of natural numbers but doesn't elaborate on it.