3

I suspect that teyjus, the main implementation of λProlog, might be a bit of abandonware, but λProlog is a fascinating Prolog that is supposed to let you use higher-order logic, hypothetical reasoning and other things, which is why I'm trying to use it.

File "example.sig":

sig example.

kind person, language type.

type hans person.
type german, french, italian language.

type grade person -> o.
type take person -> language -> o.

File "example.mod":

module example.

(grade P) :- (take P german), (take P french).
(grade P) :- (take P german), (take P italian).

take hans french.

However, when I compile and load it, while it appears to work, hypothetical reasoning queries get rejected:

[example] ?- take X Y.

The answer substitution:
Y = french
X = hans

More solutions (y/n)? y

no (more) solutions

[example] ?- grade X.

no (more) solutions

[example] ?- (take hans german) => (grade hans).
(1,19) : Error : Symbol => is not permitted within terms

I was expecting a "yes" at the end there. What am I doing wrong?

MWB
  • 11,740
  • 6
  • 46
  • 91
  • Is your parenthetization of the Harrop Formula correct? `memb 1 (1 :: nil) => memb 1 (2 :: 1 :: nil) & memb 1 (1 :: nil)` is allowed – David Tonhofer Dec 07 '20 at 06:41
  • I guess a lot of work goes into Bedwyr these days (logic programming in linear logic) – David Tonhofer Dec 07 '20 at 06:44
  • @DavidTonhofer `Is your parenthetization of the Harrop Formula correct?` I think so. `is allowed` in *.mod or in the interpreter? did you try it? `tjsim --version` ? – MWB Dec 07 '20 at 06:50
  • 1
    No, sorry. I just have [the book](https://www.cambridge.org/core/books/programming-with-higherorder-logic/90460BBDEF7ADE2B2B738DD05A39ECC5#) :-( – David Tonhofer Dec 07 '20 at 10:53
  • @DavidTonhofer is the book good? Our library has just one hardcopy which is also permanently lended. I conclude the book is very specialized. – DuDa Dec 07 '20 at 22:44
  • @Raubsauger Try installing teyjus first. I'm on Ubuntu18.04, and it wasn't easy (compiled from source, had to edit makefiles, etc. a lot) I'm curious if others can reproduce the problem I described in this question. – MWB Dec 07 '20 at 22:51
  • @Raubsauger It's really very compact. It could have used some practical examples and clearly assumes that the reader has research background and can feel his/her way around the syntax (even getting the hand of the typing syntax gave me trouble). In the end I couldn't think of an reasonably applicable advantage of Lambda-Prolog (there needs to be an "The Art of Lambda-Prolog"). Consider it an expanded version of the paper [Higher-Order Logic Programming](https://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.160.7209) ... – David Tonhofer Dec 07 '20 at 23:08
  • ... which appears in [Handbook of Logic in Artificial Intelligence and Logic Programming](https://global.oup.com/academic/product/handbook-of-logic-in-artificial-intelligence-and-logic-programming-9780198537922?lang=en&cc=lu#) which is GBP 390 WTF? Sellers offer "Programming with HOL" at [amazon.com](https://www.amazon.com/Programming-Higher-Order-Logic-Dale-Miller-ebook/dp/B009ZRNPZG/ref=sr_1_1?dchild=1&keywords=miller+nadathur&qid=1607382614&sr=8-1) for USD 40.... – David Tonhofer Dec 07 '20 at 23:11
  • ... though there is also an offer for USD 900, which is either a crazy bot in a self-reinforcing loop or a payment scheme for extra-legal services (or so I hear). The PDF of the book is also floating around on the interwebs (cough). – David Tonhofer Dec 07 '20 at 23:12
  • @DavidTonhofer Thanks for the link, I wanted to have a glimpse. I'm actually impressed how many computer science papers are free (without coughing). The Handbook is available in my library. – DuDa Dec 07 '20 at 23:23
  • @Raubsauger Indeed. I'm a heavy collector ... notice that HOL paper can be downloaded from the link given. – David Tonhofer Dec 07 '20 at 23:27
  • @DavidTonhofer *"In the end I couldn't think of an reasonably applicable advantage of Lambda-Prolog"* Might be a good time to ask for some examples, while the author of the book is here :-) – MWB Dec 13 '20 at 09:52
  • @MaxB Holy damn Dale Miller himself! But this is not the time ... (Next on that branch: Reading ["An Overview of Linear Logic Programming"](https://www.researchgate.net/publication/2603027_An_Overview_of_Linear_Logic_Programming) (Dale Miller 2003)). – David Tonhofer Dec 13 '20 at 10:08

2 Answers2

5

The current version of Teyjus does not allow implications in queries to be entered directly to the top-level. The book by Gopalan Nadathur and me (Programming with Higher-Order Logic) mentioned this problem and a workaround in the Appendix (see excerpt below).

A.4.2 Deviations from the language assumed in this book (page 287)

[...]

Teyjus does not permit implications to be used in top-level goals. This is a characteristic that may change in the future when the compilation model is extended also to these goals but, for now, it means that some of the examples presented, eg, in Section 3.2, cannot be run directly using this system. Notice that implications are disallowed only in top-level goals: they can be used freely in goals that appear in the body of program clauses. Thus, this limitation can be overcome by first building a suitable program clause and then using it to pose the desired query. For example, instead of posing the query

?- p a => p b => p X.

one can create the clause

test X :- p a => p b => p X.

and then use the query

?- test X.
Dale Miller
  • 186
  • 3
  • Thanks for the answer! Another Q you might be interested in: (Although it has answers, I do not know how complete they are) https://stackoverflow.com/questions/65084003 – MWB Dec 13 '20 at 10:00
2

Extend "example.sig" by:

type whatif language -> o.

Extend "example.mod" by:

(whatif Q) :- ((take hans Q) => (grade hans)).

And then it works:

enter image description here

Looks like λProlog is lazyware, I raised an issue #122.
Or there are some fundamental problem that it doesn't work,
like typing problems or compiler optimizations?

P.S.: I was living dangerously, and downloaded tjsim.exe etc.. from here:
http://www.eecs.ucf.edu/~leavens/Windows/usr-local-bin/

  • I had to change the GitHub ticket into a feature request first, but its linked again. –  Dec 13 '20 at 09:08