proj-plbook-plChLogicLangs

Logic

Prolog

Attributes:

Influences: "The predecessor of Prolog was a wonderful thing that Carl Hewitt did in the late 1960s called Planner." -- Alan Kay, http://queue.acm.org/detail.cfm?id=1039523

Tutorials and books:

Opinions:

Applications:

Implementations:

Probabalistic Prolog

https://dtai.cs.kuleuven.be/problog/

MiniZinc

https://www.minizinc.org/

Picat

Examples

(from [5]) input_data(Tri) reads rows of integers from the text file triangle.txt into an array:

import util.

input_data(Tri) => 
    Lines = read_file_lines("triangle.txt"),
    Tri = new_array(Lines.length),
    I = 1,
    foreach(Line in Lines)
        Tri[I] = Line.split().map(to_integer).to_array(),
	I := I+1
    end.

(from [6]) input_data(Tri) reads rows of integers from the text file triangle.txt into an array:

returns a list of all of the permutations of L:

perms([]) = [[]].
perms(L) = [[E|P] : E in L, P in perms(L.delete(E))].

(from [7]) Given a triangle stored in an array, solves https://projecteuler.net/problem=67 ; the first line is a table mode declaration that instructs the system about how to table the calls and answers: + means that the argument is tabled, max means that the argument should be maximized, and nt means that the argument is not tabled. This predicate searches for a path with the maximum total sum. If the current row is at the bottom of the triangle, then the leaf value is returned. Otherwise, it makes a non-deterministic choice between two branches, one going straight down and the other going down to the adjacent number.:

table (+,+,max,nt) 
path(Row,Col,Sum,Tri),Row==Tri.length => Sum=Tri[Row,Col].
path(Row,Col,Sum,Tri) ?=> 
    path(Row+1,Col,Sum1,Tri),
    Sum = Sum1+Tri[Row,Col].
path(Row,Col,Sum,Tri) => 
    path(Row+1,Col+1,Sum1,Tri),
    Sum = Sum1+Tri[Row,Col].    

Links:

Tabled logic programming uses memoization to alleviate these problems by avoiding infinite and redundant paths of computation. The central data structure is a table in which we store encountered subgoals and corresponding solutions. When we solve a subgoal G, then we check whether G is in the table. If it is not in the table, then it will be added. If it is in the table and there are solutions available, then we can re-use them. If it is in the table and no solutions are available, then we suspend the computation. This basic idea is combined with global stages. In each stage, a depth-first search strategy is used to derive answers from the program. If no more answers can be derived, computation terminates. It is important to note that for each answer only one proof is generated, although multiple different proofs may exist. " -- [8]

Ciao

https://en.wikipedia.org/wiki/Ciao_%28programming_language%29

Curry

https://en.wikipedia.org/wiki/Curry_%28programming_language%29

functional logic

Mercury

https://en.wikipedia.org/wiki/Mercury_%28programming_language%29

functional logic

miniKanren

" miniKanren is a family of programming languages for relational programming.[1] As relations are bidirectional, if miniKanren is given an expression and a desired output, miniKanren can run the expression "backward", finding all possible inputs to the expression that produce the desired output. This bidirectional behavior allows the user to constrain both the input to the program and the result of the program simultaneously. miniKanren performs an interleaved search which will eventually find any solution that exists, even if any one branch of the search tree is infinitely long and contains no solutions. If no solution exists, miniKanren may search forever if the search tree is infinite.

An example of miniKanren code is evalo, a relational goal that relates expressions to the values that they evaluate to. When evalo is called in miniKanren like so: (evalo q q), it will generate quines, that is, expressions q that when run will evaluate to themselves.[2]

The book The Reasoned Schemer uses miniKanren to demonstrate relational programming, and provides a complete implementation in Scheme.[3] The core of the language fits on two printed pages. The Scheme implementation of miniKanren is designed to be easily understood, modified, and extended.

αleanTAP is a program written in αKanren, an extension of miniKanren for nominal logic. Given a theorem, it can find a proof, making it a theorem-prover. Given a proof, it can find the theorem, making it a theorem-checker. Given part of a proof and part of a theorem, it will fill in the missing parts of the proof and the theorem, making it a theorem-explorer.[1]

There are implementations of miniKanren in Haskell, Racket, Ruby, Clojure, and Python. The canonical implementation is an embedded language in Scheme. The Clojure core.logic library was inspired by miniKanren.

The name kanren comes from a Japanese word for "relation". " -- https://en.wikipedia.org/wiki/MiniKanren

" miniKanren is an embedded Domain Specific Language for logic programming.

The core miniKanren language is very simple, with only three logical operators and one interface operator. The core language, using Scheme as the host language, is described in this short, interactive tutorial.

miniKanren has been implemented in a growing number of host languages, including Scheme, Racket, Clojure, Haskell, Python, JavaScript?, Scala, Ruby, OCaml, and PHP, among many other languages.

miniKanren is designed to be easily modified and extended; extensions include Constraint Logic Programming, probabilistic logic programming, nominal logic programming, and tabling.

A detailed discussion of the differences between miniKanren and Prolog can be found here. " -- http://minikanren.org/

"

Core miniKanren extends Scheme with three operations: ==, fresh, and conde. There is also run, which serves as an interface between Scheme and miniKanren, and whose value is a list.

unifies two terms. fresh, which syntactically looks like lambda, introduces lexically-scoped Scheme variables that are bound to new logic variables; fresh also performs conjunction of the relations within its body. Thus

(fresh (x y z) (== x z) (== 3 y))

  1. <procedure>

would introduce logic variables x, y, and z, then associate x with z and y with 3. This, however, is not a legal miniKanren program---we must wrap a run around the entire expression.

(run 1 (q) (fresh (x y z) (== x z) (== 3 y)))

(_.0)

The value returned is a list containing the single value (_.0); we say that _.0 is the reified value of the unbound query variable q and thus represents any value. q also remains unbound in

(run 1 (q) (fresh (x y) (== x q) (== 3 y)))

(_.0)

We can get back more interesting values by unifying the query variable with another term.

(run 1 (y) (fresh (x z) (== x z) (== 3 y)))

(3)

...the y introduced by fresh is different from the y introduced by run....

A run expression can return the empty list, indicating that the body of the expression is logically inconsistent. ... conde, which resembles cond syntactically, is used to produce multiple answers. Logically, conde can be thought of as disjunctive normal form: each clause represents a disjunct, and is independent of the other clauses, with the relations within a clause acting as the conjuncts. For example, this expression produces two answers.

(run 2 (q) (fresh (w x y) (conde ((== `(,x ,w ,x) q) (== y w)) ((== `(,w ,x ,w) q) (== y w)))))

((_.0 _.1 _.0) (_.0 _.1 _.0))

Although the two conde lines are different, the values returned are identical. This is because distinct reified unbound variables are assigned distinct subscripts, increasing from left to right—the numbering starts over again from zero within each answer, which is why the reified value of x is _.0 in the first answer but _.1 in the second. The argument 2 in run denotes the maximum length of the resultant list. If run* is used instead, then there is no maximum imposed. This can easily lead to infinite loops.

(run* (q) (let loop () (conde ((== #f q)) ((== #t q)) ((loop)))))

error: (124) inifinite loop!

If we replace * by a natural number n, then an n-element list of alternating #f's and #t's is returned. The first answer is produced by the first conde clause, which associates q with #f. To produce the second answer, the second conde clause is tried. Since conde clauses are independent, the association between q and #f made in the first clause is forgotten---we say that q has been refreshed. In the third conde clause, q is refreshed again. ... " -- http://io.livecode.ch/learn/webyrd/webmk

tutorials and books:

muKanren

http://webyrd.net/scheme-2013/papers/HemannMuKanren2013.pdf

" miniKanren is the principal member of an eponymous family of relational (logic) programming languages. Many of its critical design decisions are a reaction to those of Prolog and other well-known 5th-generation languages. One of the differences is that, while a typical Prolog implementation might be thousands of lines of C code, a miniKanren language is usually implemented in somewhere under 1000 lines. Though there are miniKanren languages of varied sizes and feature sets (see http://miniKanren.org ), the original published implementation was 265 lines of Scheme code. In those few lines, it provides an expressiveness comparable to that of an implementation of a pure subset of Prolog. We argue, though, that deeply buried within that 265-line miniKanren implementation is a small, beautiful, relational programming language seeking to get out. We believe μKanren is that language. By minimizing the operators to those strictly necessary to do relational programming and placing much of the interface directly under the user's control, we have further simpli ed the implementation and illuminated the role and interrelationships of the remaining components. By making the implementation entirely functional and devoid of macros, heretofore opaque sections of the system's internals are made manifest. What is more, by re-adjudicating what functions are properly the purview of the end user, we develop an implementation that weighs in at 39 lines of Scheme.

The μKanren Language

Herein, we briefy describe the syntax of μKanren programs, with a focus on those areas in which μKanren differs from earlier miniKanren languages. Readers intimately familiar with miniKanren programming may lightly peruse this section; readers seeking a thorough introduction to miniKanren programming are directed to Byrd and Friedman et. al, from which the present discussion is adapted. A μKanren program proceeds through the application of a goal to a state . Goals are often understood by analogy to predicates. Whereas the application of a predicate to an element of its domain can be either true or false, a goal pursued in a given state can either succeed or fail . A goal's success may result in a sequence of (enlarged) states, which we term a stream. We use functions to simulate relations. An arbitrary n-ary relation is viewed as an (n - 1)-ary partial function, mapping tuples of domain elements into a linearized submultiset of elements of the codomain over which the initial relation holds. A given collection of goals may be satis ed by zero or more states. The result of a μKanren program is a stream of satisfying states. The stream may be finite or infinite, as there may be finite or infinitely many satisfying states. A program's resulting stream thus depends on the goals that comprise that program. In μKanren there are four primitive goal constructors:

The == goal constructor is the primary workhorse of the system; goals constructed from == succeed when the two arguments unify. The success of goals built from == may cause the state to grow. Unlike the implementation of == detailed in Friedman et. al, that presented here does not prohibit circularities in the substitution.

The call/fresh goal constructor creates a fresh (new) logic variable. call/fresh 's sole argument is a unary function whose binding variable is a fresh logic variable and whose body is an expression over which the fresh variable's binding is scoped and which evaluates to a goal.

The disj and conj goal constructors express a sort of boolean logic over goals; they represent the binary disjunction and conjunction of goals, respectively. That is, both take two goals as arguments. A goal constructed from disj returns a non-empty stream if either of its two arguments are successful, and a goal constructed from conj returns a nonempty stream if the second argument can be achieved in the stream generated by the first. "

muKanren implementations:

Z3.py

example usage: https://www.zellic.io/blog/formal-verification-weth

datalog

related to Prolog

souflle

https://souffle-lang.github.io/

related to Datalog

Links