3 ms·

Abstract Machines for Logic Programs

58 points by surprisetalk 6mo ago

Twisol 6mo ago
> 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 https://link.springer.com/chapter/10.1007/11431664_4
tannhaeuser 6mo ago
> Here is a stack machine that [instead of addition] implements subtraction, based on the mode assignment i/o/i [without changing the code already used for addition]. (You might have heard people claim that logic programs can be "run backwards"; this is one thing that can mean.) k >> plus 0 _ P |----> k << P k >> plus (s N) _ (s P) |----> k; _ >> plus N _ P k; _ << P |----> k << P So if you're confused because of the slightly unusual notation, here's the same thing in Prolog syntax: % "Sum is the sum of S1 and S2" plus(S1, S2, Sum) :- Sum is S1 + S2. % "What is the sum of 3 and 5?" ?- plus(3, 5, S). % Answer: S = 8 % "Is 10 the sum of 3 and 5" ?- plus(3, 5, 10). % Answer: fail % "What's the difference between 3 and 10?" ?- plus(3, X, 10). % throws an error 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.
- upghost 6mo ago
  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.
gobdovan 6mo ago
[dead]

58 points by surprisetalk 6mo ago

> 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 https://link.springer.com/chapter/10.1007/11431664_4

tannhaeuser 6mo ago

> Here is a stack machine that [instead of addition] implements subtraction, based on the mode assignment i/o/i [without changing the code already used for addition]. (You might have heard people claim that logic programs can be "run backwards"; this is one thing that can mean.) k >> plus 0 _ P |----> k << P k >> plus (s N) _ (s P) |----> k; _ >> plus N _ P k; _ << P |----> k << P So if you're confused because of the slightly unusual notation, here's the same thing in Prolog syntax: % "Sum is the sum of S1 and S2" plus(S1, S2, Sum) :- Sum is S1 + S2. % "What is the sum of 3 and 5?" ?- plus(3, 5, S). % Answer: S = 8 % "Is 10 the sum of 3 and 5" ?- plus(3, 5, 10). % Answer: fail % "What's the difference between 3 and 10?" ?- plus(3, X, 10). % throws an error 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.

upghost 6mo ago
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.

gobdovan 6mo ago

[dead]