Stack Overflow
Stack Overflow

Questions tagged [lambda-prolog]

λProlog is a logic programming language based on an intuitionistic fragment of Church's Simple Theory of Types, featuring polymorphic typing, modular programming, abstract datatypes, support for lambda-tree syntax, and higher-order programming.

λProlog(LambdaProlog)

λProlog is a logic programming language based on an intuitionistic fragment of Church's Simple Theory of Types. Such a strong logical foundations provides λProlog with logically supported notions of

  1. modular programming,

  2. abstract datatypes

  3. higher-order programming, and

  4. the lambda-tree syntax approach to the treatment of bound variables in syntax.

Implementations of λProlog make use of simply typed λ-terms as well as (of subsets) of higher-order unification.

Its simplicity makes it especially appropriate for teaching, where it can help provide the students with a high-level and direct language for implementing, for example, inference based systems, grammars, automata, etc.

For more information and resources, visit the official λProlog site.

Coding in λProlog

Many languages implement the concepts behind λProlog. Teyjus is one of the most maintained and advanced such languages. Visit the official Teyjus site for more information, including download instructions. There are a couple of emacs modes for developing using Teyjus available through a Google search.

Learning λProlog

To delve into the theoretical foundations of λProlog, the main reference is the Programming with Higher-Order Logic book. For light and introductory tutorials, one can find various resources ranging in difficulty, both in written and video form, on the official λProlog site.

13 questions
21
votes
4 answers

What is more interesting or powerful: Curry, Mercury or Lambda-Prolog?

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…
Bubba88
  • 1,910
  • 20
  • 44
4
votes
3 answers

Pure Prolog Scheme Quine

There is this paper: William E. Byrd, Eric Holk, Daniel P. Friedman, 2012 miniKanren, Live and Untagged Quine Generation via Relational Interpreters http://webyrd.net/quines/quines.pdf Which uses logic programming to find a Scheme Quine.…
user502187
4
votes
1 answer

Is there a higher order Prolog that wouldn't need a type system?

I suspect that λProlog needs a type system to make their higher order unification sound. Otherwise through self application some Russell type anomalies can appear. Are there alternative higher order Prologs that don't need .sig files? Maybe by a…
user502187
4
votes
2 answers

higher-order "solutions" predicate

I am using a higher order Prolog variant that lacks findall. There is another question on implementing our own findall here: Getting list of solutions in Prolog. The inefficient implementation is: parent(pam, bob). %pam is a parent of…
mrsteve
  • 4,082
  • 1
  • 26
  • 63
4
votes
1 answer

Errors installing OMake on OSX 10.10.5

I'm trying to install OMake so I can install Teyjus so I can start writing a bit of Lambda Prolog but I'm getting I'm getting a bunch of errors on OS X 10.10.5. The most current one, that I can't figure out, is: *** omake: 497/1193 targets are up to…
king_geedorah
  • 91
  • 8
3
votes
2 answers

λProlog rejecting hypothetical reasoning queries?

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…
MWB
  • 11,740
  • 6
  • 46
  • 91
2
votes
0 answers

Clauses in (lambda)prolog starting with a cut

I am reading the paper Implementing Type Theory in Higher Order Constraint Logic Programming, and on p7 I see the following lambda-prolog code: % KAM-like rules in CPS style whd1 (app M N) S Ks Kf :- !, Ks [] M [N|S]. whd1 (lam T F1) [N|NS] Ks Kf :-…
Mike Shulman
  • 165
  • 7
2
votes
1 answer

λProlog hypothetical reasoning Tic Tac Toe

λProlog features hypothetical reasoning. By using the operator (=>)/2 we can temporarily assert some clause. Can this be used to realize adversarial search in λProlog? Was thinking about Tic-Tac-Toe game. Instead of starting with cell/3 facts that…
user502187
2
votes
2 answers

De Bruijn index based substitution in Prolog

The Dutch mathematician Nicolaas Govert de Bruijn invented these indexes for representing terms of lambda calculus without naming the bound variables. Lets take this lambda expression: K = λx.λy.x With de Bruijn indexes it reads, when we use the…
user502187
2
votes
2 answers

Is there any difference between an N-ary function in Curry and an N+1-ary relation in Prolog?

Curry, unlike its cousin Haskell, allows you to give multiple values to a function: foo 1 2 = 3 foo 1 2 = 4 and it does backtracking (or some other search) to explore the implications of such non-determinism. This makes it similar to Prolog…
MWB
  • 11,740
  • 6
  • 46
  • 91
1
vote
2 answers

What does higher-order semantics give you in λProlog?

λProlog is a higher-order dialect of Prolog. On the other hand, HiLog is said to use higher-order syntax with first-order model theory. In other words, they both have higher-order syntax, but only λProlog has higher-order semantics. What does…
MWB
  • 11,740
  • 6
  • 46
  • 91
1
vote
2 answers

List comprehension in Lambda Prolog

I'm using Teyjus for programming in Lambda Prolog. I have this simple lists generator: type islist int -> list X -> o. islist N nil :- N >= 0. islist N (H::T) :- N >= 0, M is N - 1, islist M T. I need to create a…
Marco Mantovani
  • 111
  • 2
  • 7
0
votes
2 answers

Reverse Conversion in Prolog

Would like to do the follow reverse conversion from SKI expressions to lambda expressions: L[I] = λx.x L[K] = λx.λy.x L[S] = λx.λy.λz.(x z (y z)) L[(E₁ E₂)] = (L[E₁] L[E₂]) The conversion need not involve any beta-reduction. But I would…
user502187