How to implement a prolog interpreter in a purely functional language?

Question Detail: 

Is there a clear reference, with pseudo-code, on how to go about implementing a Prolog interpreter in a purely functional language? That which I have found so far seems to deal only with imperative languages, is merely a demonstration of Prolog implemented in itself, or offers no concrete algorithm to use for interpretation. I would be very appreciative of an answer.

Asked By : Jimster

Best Answer from StackOverflow

Question Source : http://cs.stackexchange.com/questions/6618

Answered By : Guy Coder

Since Prolog = Syntactic Unification + Backward chaining + REPL

All three parts can be found in Artificial intelligence: structures and strategies for complex problem solving by George F. Luger. In the fourth edition of the book all three parts are implemented in LISP in Section 15.8, Logic Programming in LISP. He also puts the same code in his other books, but I don't have all of them for noting here. The code for his books can be found here.

Another source with all three parts can be found in Paradigms of artificial intelligence programming: case studies in Common Lisp by Peter Norvig. See Chapters 11, Logic Programming and 12, Compiling Logic Programs. The code for his book can be found here.

Another source is Structure and interpretation of computer programs by Hal Abelson, Jerry Sussman and Julie Sussman. See Section 4.4 Logic Programming. The site for the book is here and the code for the book is here.

It is not uncommon to find the unification algorithm with back chaining implemented in many applications if you know where to look; it is especially prevalent in type inferencing in functional compilers. Using the keywords unification or occurs helps to spot the functions. Also most implementations use unif for the name of the unification function.

For a version of Prolog, less the REPL, done in OCaml see Code and resources for "Handbook of Practical Logic and Automated Reasoning" - prolog.ml

A translation of the book code to F# can be found here. A translation of the book code to Haskell can be found here.

In terms of finding the code, the unification algorithm is easiest to find, then implementations with back chaining imbedded in applications. Finding a fully functional implementation of Prolog in a functional language with an REPL is the hardest. Most of the time the code is not in a format for direct use within PROLOG; it is heavily customized to enhance performance, so you may find the code but it will not be worth the price to tease out the parts you want. My advice would be to read Luger's book and build it up from scratch in your language of choice, even if it means installing and learning LISP and translating to do so.

EDIT

Since this is a duplicate question from StackOverflow and the OP is new and in the comments says:

To give more context, I'm attempting to implement type inference, however the intricate features in the type system of my language (Dependent types, refinement types, linear typing to name a few of the less common ones) make me feel that it would be useful to base my type inference off of the algorithms driving Prolog as to obtain a very general algorithm. I will note that I'm entirely self taught, so my knowledge is lacking in large areas.

I'll expand on this here, but realize the OP should ask a new question.

For some intro stuff see implementing type inference.

The best book I know on this is Types and programming languages by Benjamin C. Pierce. The book's site is here. The resources with links to OCaml code is here. And recently started but mostly complete translation of this to F# is here.

Dependent types: pg. 462 Refinement types: pg. 207 Linear logic and type systems: pg. 109