Help Wanted -- Mapping Prolog terms to Lisp forms and vice versa

[jjtolton]

Hello everyone! For libscryer-clj, I'm trying to work on an isomorphic mapping between a subset of ISO Prolog and lisp forms. If anyone has any thoughts or prior art to point to, please feel free to share here or on the libscryer-clj discussion.

(Regarding syntax: this is meant to be a truly isomorphic effort, I do not want to lose any of the syntactic power of pure ISO prolog. The API will be such that you can transparently meta-interpret either syntax with a mostly invisible adapter abstraction. Deviating from ISO prolog syntax is an anti-goal.)

[triska]

An initial suggestion for the term p(f(X,a), Y, "abc"):

(compound "p" (compound "f" (var "X") (atom "a"))
              (var "Y")
              (compound "." (atom "a") (compound "." (atom "b") (atom "[]"))))

[triska]

(With opportunities for abbreviations, such as (string "abc").)

[jjtolton]

Interesting. So I think this brings up a good point -- there should probably be a "canonical" representation that is hopefully close to either the Prolog canonical representation OR the ABI representation as envisioned by @bakaq and @Skgland. In addition, I think a more ergonomic DSL might be warranted, but I am concerned I am missing obvious issues. For insance --

Would

(p (f ?x "a") ?y "abc")

be insufficient as a higher level abstraction (above the canonical layer) for the term you suggested?

[hurufu]

I think @bakaq recently implemented a protocol to communicate with top-level. Doesn't it server the same purpose?

[bakaq]

If you mean #2527, that is inside Prolog itself so I think it doesn't apply here. The closest to this was the discussions about the JSON serialization in #2493 and #2707, which has many of the same problems.

Would

(p (f ?x "a") ?y "abc")

be insufficient as a higher level abstraction (above the canonical layer) for the term you suggested?

Well, to start, this is ambiguous because it is representing atoms and strings the same way, so not injective and therefore not isomorphic.

[jjtolton]

This is exactly the kind of feedback I'm looking for and the sort of trap I'm trying to avoid! I'm actually unclear on how this is ambiguous, but I know you've studied this problem intensively.

[hurufu]

Univ operator =.. establishes an equivalence between arbitrary terms and lists. If you can represent arbitrary lists in Clojure then you can just use it, but it doesn't address representation of logic variables – the hard part.

[jjtolton]

Oh interesting! What is that syntax? is that KIF or GDL?

[hurufu]

Game description language is an abstract set of valid rules and operators, but KIF is the "transport encoding" to send game descriptions between heterogeneous solvers.

[jjtolton]

https://en.wikipedia.org/wiki/Knowledge_Interchange_Format

The designers of KIF likened it to PostScript.

Sounds promising!

[hurufu]

Here is an example program in KIF notation. I never bothered to read specification, but this exact text was accepted by solvers – so it is good to go.

offtopic: Don't expect much from GDL – progress has stopped 15 years ago without producing any immediately useful results. And all research switched from symbolic AI to ML. You will be hugely disappointed if your would use GDL, both in terms of performance and sophistication.

[jjtolton]

@hurufu this actually looks pretty good. I found a copy of the KIF manual (in PostScript!) and I'm going through it.

[bakaq]

Strictly speaking, I don't know if you can have an (ergonomic) isomorphism actually, because of stuff like []. It's an atom, but it's also a list, so for example (assuming an obvious mapping) () and (atom "[]") would both map to [], making it not injective, and therefore certainly not an isomorphism. It's even worse if you consider that this is also the empty string "".

The only way I can see this actually being an isomorphism is not using any syntax sugar and working with something close to the canonical representation of terms (like @triska suggested above). This would mean no lists for example, which is very unfortunate and unergonomic.

[bakaq]

I think what is being said here is that in Prolog .(a, "bc") and "abc" are literally the same thing, while in Clojure (. a "bc") and [a | "bc"] are really 2 different things. If they both map to .(a, "bc")/"abc" then the map is not injective and therefore isn't an isomorphism.

?- .(a, "bc") == [a | "bc"].
   true.

user=> (= '(. a "bc") '[a | "bc"])
false

[triska]

?- .(a, "bc") == "abc".
   true.

[jjtolton]

I think what is being said here is that in Prolog .(a, "bc") and "abc" are literally the same thing, while in Clojure (. a "bc") and [a | "bc"] are really 2 different things. If they both map to .(a, "bc")/"abc" then the map is not injective and therefore isn't an isomorphism.

?- .(a, "bc") == [a | "bc"].
   true.

user=> (= '(. a "bc") '[a | "bc"])
false

Ah, yes, got it.

I'm struggling with terminology here. Maybe syntactically isomorphic is incorrect or irrelevant. The important thing is that they are semantically isomorphic, perhaps?

Please take a look at the diagram to help understand the equivalency I am trying to establish. All these points are well founded, and my imprecise terminology is causing confusion.

Basically, for a given "underlying" canonical(??) semantic concept, I'm trying to establish a mapping between a family/set of Prolog terms to a family/set of Clojure forms, all of which are acceptable because they should unify.

So for any given canonical(??) semantic concept, there should be a set of Prolog terms that maps to a set of Clojure Forms, but they are semantically (if not syntactically) equivalent.

[jjtolton]

In fact, we could imagine a predicate:

prolog_clojure(PrologTerm, ClojureString)

that holds if and only if the PrologTerm semantically unifies with the ClojureString

[jjtolton]

Interesting, now that I think about it, I'm willing to bet the whole concept of unification is significantly deeper than I initially thought 🤔

[jjtolton]

This seems interesting:

Unique Features of Lisp Machine Prolog

[UWN]

This seems interesting:

Unique Features of Lisp Machine Prolog

TIL, 3.1, p. 4: LM-Prolog allows the user to control whether the occur check is
done or not, or whether cyclic structures should be anticipated.

This is quite surprising, since the system immediately succeeding LM-Prolog is SICStus which does not have this option. Fortunately, Scryer has it.

[jjtolton]

Interesting. It was mentioned alongside LogLisp and something called Allegro Prolog -- Allegro Prolog doesn't seem to use Prolog syntax, though.

[jjtolton]

Thanks to @hurufu, found this scary link to a postscript version of the KIF manual

[hurufu]

Cool, I actually have never read it, I saw KIF just as an obstacle on my way to use use 3rd party solvers :) Also I used some converter written in Java from a special syntactic variant of Prolog to KIF.

[jjtolton]

Update: I think I've found a reasonable approach using DCGs, and working towards it incrementally. I'm working on a predicate

scryer_clojure(ScryerString, ClojureString)

which, as the name implies, relates a valid Scryer Prolog string to a valid Clojure String.

I am currently using DCGs to make a lexer, and the parser will come next.

[jjtolton]

Ok, I created an initial executable spec for the lexer. It's certainly not finished, incremental progress towards increasingly complex examples. It's very close to @triska 's initial proposal -- I currently used lists instead of increasing arrity for the lexer just because it was a little easier for me.

I'm very open to suggestions for test cases, pull requests, general strategy and/or tactics.

Particularly valuable would be things like "can your syntax handle this" or "can your syntax handle that".

Obviously it can only handle a subset of Prolog right now, but I'd like to incrementally expand it.