Is λProlog a strict superset of Prolog/WAM?

[emummel20]

Hey, hopefully a quick question on extending Scryer with Lambda Prolog:

Reading this description of the Teyjus implementation, they mention some additional features that should be accommodated in the λProlog compiler

• The language contains primitives that can alter the name space and the definitions of procedures in the course of execution. This means, in particular, that unification has to pay attention to changing signatures and that the solution to each (sub)goal has to be relativized to a specific program context.
• In contrast to other languages, lambda terms are used in Lambda Prolog as data structures. A representation must therefore be provided for these terms that permits their structures to be examined and compared in addition to supporting reduction operations efficiently.
• Higher-order unification is used in an intrinsic way in the language. This operation has a branching character that must be supported. Further, it is sometimes preferable to delay the solution to unification problems and so a good method is needed for transmitting these across computation steps.
• In addition to having a role in determining program correctness, types are relevant to the dynamic behavior of programs. A sensible scheme must therefore be included for carrying these along at run-time.
• Programming in the language is done relative to modules. In realizing this feature, it is necessary to support certain operations for composing different modules. Moreover, a mechanism must be provided for periodically adding and removing code depending on which modules are in use.

In your estimation, how difficult would it be to fork Scryer in order to implement λProlog? Is λProlog a proper superset of Prolog and you could simply build on top of Scryer or would the compiler need to be different enough that it wouldn't make sense to fork Scryer for this? Thanks

[philzook58]

This is somewhat tangential, but I know prolog experts see this.
I've spent some amount of time and thought trying to figure out how to shallowly embed lambda prolog capabilities (even just harrop clauses) into a standard Prolog and am basically stumped. I thought at first the assert/retract predicates could be used to perform implication, but on deeper thought they don't behave correctly on branch failure, nor do they maintain their unification variables connection to those in the environment. Encoding into CHR might be possible but is baroque. In addition, reusing host prolog unification doesn't seem to work because it is too hard to reliably achieve scope escaping checks (maybe attributed variables could help? I'm not sure). gensym might work ok-ish for harrop foralls.
It seems like the best thing to do is write a lambda prolog interpreter and borrow almost no capabilities from the host prolog. This is surprising and disappointing, but even then a well thought out library would be appreciated. It would be nice to be able to use a mature prolog implementation with it's performance and ecosystem in a context where lambda prolog is useful (theorem proving mostly I suppose https://github.com/LPCIC/coq-elpi https://rust-lang.github.io/chalk/book/clauses.html ).
Suggestions very much appreciated.

[philzook58]

backtrackable assignment like b_setval looks possibly useful. I don't see how it immediately solves the problems though. Maybe this shallow embedding approach is a leaky sieve that will never work. It is just a bit surprising how far lambda prolog is from regular prolog.

[emummel20]

It is just a bit surprising how far lambda prolog is from regular prolog.

Hence my question :D Appreciate your input.

[emummel20]

@philzook58 if it's not a secret, would you mind sharing your attempt to implement implications in prolog? I'd love to see.

[philzook58]

@emummel20 I wrote up some notes on my attempts in this direction https://www.philipzucker.com/harrop-checkpoint/ Using intercept / delimited continuations is the most interesting shallow encoding I know of so far

[emummel20]

@philzook58 sorry I totally missed this comment, appreciate the blog post. I'm still working my way through it but it sounds like long story short, it's not exactly possible to implement hhc as cleanly as you would have them in λProlog?

Can you provide an example where setup_call_cleanup/3 wouldn't work? You mentioned it wouldn't because retract only runs once but why would you need it to run more than once? Do you mean if you are asserting more than one fact in the setup arg like this?

setup_call_cleanup((assert(foo(557)),assert(foo(123))),foo(X),retract(foo(_))).

because if so then yes you would still be left with one of the assertions at the end of it, but if you use retractall like this instead

setup_call_cleanup((assert(foo(557)),assert(foo(123))),foo(X),retractall(foo(_))).

then of course they're all retracted.

Can you clarify? Thanks.

[emummel20]

Or let me ask it a different way: Are the additional features of λprolog orthogonal enough to scryer that it could be worked on in rust in parallel and then submitted as a pull req? Or is it so integrated and would it require so many changes to the core code that a fork would be required to make it work?

Also would like to bump the question of, would it be possible to implement λprolog in prolog itself?