Question

I would like to ask you about what formal system could be more interesting to implement from scratch/reverse engineer.

I ve looked through some existing and open-source projects of logical/declarative programming systems. I ve decided to make up something similar in my free time, or at least to catch the general idea of implementation.

It would be great if some of these systems would provide most of the expressive power and conciseness of modern academic investigations in logic and its relation with computational models.

What would you recommend to study at least at the conceptual level? For example, Lambda-Prolog is interesting particularly because it allows for higher order relations, but AFAIK is based on intuitionist logic and therefore lack the excluded-middle principle; that s generally a disadvantage for me.

I would also welcome any suggestions about modern logical programming systems which are less popular but more expressive/powerful.

Answer 1

Prolog was the first language which changed my point of view at programming. But later I found it to be not so high-level as I d like to see it.

Curry - I ve tried only Munster CC, and found it somewhat inconvenient. Actually, at this point, I decided to stop ignoring Haskell.

Mercury has many things which I wanted to see in Prolog. I have a really good expectation about the possibility to distinguish modes of rules. Programs written in Mercury should inspire compiler to do a lot of optimizations (I guess).

Answer 2

Twelf.

It generalizes lambda-prolog significantly, and it s a logical framework and a metalogical framework as well as a logic programming language. If you need a language with a heavy focus on logic as well as computation, it s the best I know of.

Answer 3

If I were to try to extend a logic based system, I d choose Prolog Cafe as it is small, open sourced, standards compliant, and can be easily integrated into java based systems.

Answer 4

For the final project in a programming languages course I took, we had to embed a Prolog evaluator in Scheme using continuations and macros. The end result was that you could freely mix Scheme and Prolog code, and even pass arbitrary predicates written in Scheme to the Prolog engine.

It was a very instructive exercise. The first 12 lines of code (and and or) literally took about 6 hours to write and get correct. It was pretty much the search logic, written very concisely using continuations. The rest followed a bit more easily. Then once I added the unification algorithm, it all just worked.

友情链接