13 questions
2
votes
0
answers
107
views
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 :- !...
2
votes
1
answer
129
views
λ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-...
4
votes
3
answers
512
views
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 ...
1
vote
2
answers
408
views
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
...
2
votes
2
answers
168
views
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-...
0
votes
2
answers
145
views
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 ...
4
votes
1
answer
155
views
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 ...
3
votes
2
answers
238
views
λ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 ...
1
vote
2
answers
295
views
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 ...
1
vote
2
answers
141
views
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,
...
4
votes
2
answers
515
views
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:
...
4
votes
1
answer
214
views
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 ...
21
votes
4
answers
5k
views
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/...