.
# Table of Contents
1. [Administrivia](#org944e9a2)
2. [Syntax](#org1631a81)
1. [`name` and `atom_chars`](#org01cff87)
3. [Facts & Relations](#org11a6a80)
4. [Mixfix Syntax](#org7e5c51a)
5. [Trace & Backtracking](#org7b75a05)
6. [What is a Prolog Program Exactly?](#orgd201c75)
1. [One point rule](#org67c9d9a)
2. [Overloading](#org0bf2d9a)
7. [Modus Ponens — Computation ≈ Deduction](#org3dc81b4)
8. [Conjunction ≈ Constraints — Disjunction ≈ Alternatives](#org0815789)
9. [Unification](#orgaabb8fb)
1. [Operational Semantics](#org15dfa67)
2. ['symbol' = symbol](#org8ef5c60)
3. [Unification performs no simplification, whence no arithmetic](#orga3a1299)
10. [Algebraic Datatypes](#org6447078)
11. [Arithmetic with `is` —Using Modules](#org4994886)
1. [Using Modules](#org86bbea7)
12. [Lists](#orge54ab30)
13. [Declaration Ordering Matters —Recursion](#org9e00a34)
14. [The Cut](#org0df11fd)
1. [Examples](#orgba67465)
2. [Disjoint Clauses](#org23e01e5)
3. [Conditional](#org0e85739)
4. [Cut-fail Combination](#orgdbae64d)
5. [Good Exercise](#org84fe2d7)
15. [Higher-order Support with `call`](#orgc8294a3)
16. [Meta-Programming](#org3072386)
1. [`Print, var, nonvar, arg`](#org17ed3b0)
17. [Reads](#orge425102)
# Administrivia
*Everything is a relation!* —I.e., a table in a database!
Whence programs are [unidirectional](https://blog.algorexhealth.com/2018/11/a-practo-theoretical-introduction-to-logic-programming/) and can be ‘run in reverse’:
Input arguments and output arguments are the same
thing! Only perspective shifts matter.
For example, defining a relation `append(XS, YS, ZS)`
*intended* to be true precisely when `ZS` is the catenation of `XS` with `YS`,
gives us three other methods besides being a predicate itself!
List construction: `append([1, 2], [3, 4], ZS)` ensures `ZS` is the catenation list.
List subtraction: `append([1,2], YS, [1, 2, 3, 4])` yields all solutions `YS` to
the problem `[1, 2] ++ YS = [1, 2, 3, 4]`.
Partitions: `append(XS, YS, [1, 2, 3, 4])` yields all pairs of lists that catenate
to `[1,2, 3, 4]`. **Four methods for the price of one!**
Prolog is PROgramming in LOGic. |
In Prolog, the task of the programmer is simply to *describe* problems
—write down, logically, the situation— rather than telling the computer
what to do, then obtains information by asking questions
—the logic programming system *figures out how* to get the answer.
- Prolog is declarative: A program is a collection of ‘axioms’ from which ‘theorems’
can be proven. For example, consider how sorting is performed:
- Procedurally: Find the minimum in the remainder of the list, swap it with the head
of the list; repeat on the tail of the list.
- Declaratively: `B` is the sorting of `A` *provided* it is a permutation of `A` and it is
ordered.
Whence, a program is a theory and computation is deduction!
- `swipl -s myprogram.pl` –Load your program into a REPL, `?-….`
- `make.` –Reload your program.
- `halt.` –Exit the REPL.
- `consult('CheatSheet.pl').` –Load the contents of the given file as
the new knowledge base.
- `assert(()).` –Add a new rule to the knowledge base, from within the REPL.
Use `retract(())` to remove rules from the knowledge base.
- `assert` is useful when we want to [cache](http://cs.union.edu/~striegnk/learn-prolog-now/html/node94.html#sec.l11.database.manip) computations.
- `listing.` –Display the contents of the current knowledge base; i.e.,
what Prolog ‘knows’.
- `listing(name)`. –List all information in the knowledge base about
the `name` predicate.
# Syntax
There are three types of terms:
- Constants: Numbers such as -24, and atoms such as `jasim`, `'hello world'`,
`'&^%@$ &*',` and `' '` —a space in quotes.
- Variables: Words starting with a capital letter or an underscore.
- The variable `_` is called the *anonymous variable*.
It's for when we need a variable, say when pattern matching,
but don't care about the value.
- Structures: Terms of the form `functor(term,...,term)`.
## `name` and `atom_chars`
The characters between single quotes are the *name* of an atom
and so Prolog admits `symbol = 'symbol'` as true.
- Atoms, or nullary predicates, are represented as a lists of numbers; ASCII codes.
- We can use this to compare two atoms lexicographically.
- We can obtain the characters in an atom by using the built-in `atom_chars`.
?- name(woah, X). % X = [119,111,97,104]
?- atom_chars(nice, X). % X = [n, i, c, e].
# Facts & Relations
We declare relations by having them begin with a lowercase letter;
variables are distinguished by starting with a capital letter.
/* Some facts of our world */
jasim_is_nice.
it_is_raining.
% ?- jasim_is_nice.
% true: We declared it so.
eats(fred, mangoes).
eats(bob, apples).
eats(fred, oranges).
% Which foods are eaten by fred?
% ?- eats(fred, what).
% false; “what” is a name!
% ?- eats(fred, What). % mangoes oranges
Relational constraints are formed using `:-`, which acts as the “provided”, ,
operator from logic. Read `P :- Q` as *P is true, provided Q is true.*
% All men are mortal.
mortal(X) :- man(X).
% Socrates is a man.
man(socrates).
% Hence, he's expected to be mortal.
% ?- mortal(socrates). % true
% What about Plato?
?- mortal(plato).
% false, plato's not a man.
% Let's fix that … in the REPL!
?- assert((man(plato))).
% Who is mortal?
?- mortal(X). % socrates plato
# [Mixfix Syntax](http://cs.union.edu/~striegnk/learn-prolog-now/html/node84.html#subsec.l9.operators.def)
It may feel awkward to write `father_of(homer, bart)` and instead prefer
`homer father_of bart`. We may declare relations to be prefix, infix, or postfix
with patterns `xf`, `xfx`, and `fx` respectively. For left associativity
we use pattern `yfx` and use `xfy` for right associativity.
:- op(35,xfx,father_of).
father_of(me, you).
homer father_of bart.
homer father_of lisa.
- Precedence, or binding power, is lowest at 1200 and highest at 0.
- Note: `father_of(X,Y) = X father_of Y` is true.
We may learn about existing operators too;
e.g., `?- current_op(Prec, Fixity, =:=)` ^\_^
# Trace & Backtracking
We can see what Prolog does at each step of a computation by invoking
`trace`; we turn off this feature with `notrace.`
*This’ an excellent way to learn how Prolog proof search works! (Debugging!)* |
Suppose we have the following database.
q(1). q(2). q(3).
r(2). r(3).
p(X) :- q(X), r(X).
With trace, query `p(X)` and press
*SPACE* each time to see what
Prolog is doing.
At one point, the goal `r(1)` will
*fail* and that choice \(X = 1\)
will be redone with the next possibility
for `q`, namely \(X = 2\).
The line marked `redo` is when Prolog realizes its taken the wrong
path, and backtracks to instantiate the variable to 2.
Operationally, query `p(X)` is answered by:
1. Find match for the first goal: `q` at `1`.
2. Then see if matches the second: `r` at `1`.
3. (Redo) If not, find another match for the first: `q` at `2`.
4. See if this matches the second, `r`.
5. Etc.
- `findall(X, Goal, L)` succeeds if `L` is the list of all those `X`'s for
which `Goal` holds.
- `fail/0` immediately fails when encountered. Remember: Prolog tries to
backtrack when its fails; whence `fail` can be viewed as an
instruction to force backtracking.
The opposite of forcing backtracking is to block it, which is done
with ‘cut’ `!` —see below.
# What is a Prolog Program Exactly?
A program *denotes* all true facts derivable from its clauses using
**modus ponens, unification, term rewriting, and logical or-&-and**
for the execution model.
Hidden Quantifiers:
Syntax |
Semantics |
`head(X) :- body(X,Y).` |
\( X.\, head(X) \,\, Y.\, body(X,Y)\) |
`?- Q(X)` |
\( X.\, Q(X)\) |
1. “ `head(X)` is true provided there's some `Y` such that `body(X,Y)` is true ”
- `head.` is an abbreviation for `head :- true.`
- Indeed, \(p \;≡\; (p true)\).
2. “ Is there an `X` so that `Q(X)` is true? ”
## One point rule
“One-Point Rule”: Provided `X` is a fresh variable,
## Overloading
*Overloading!* Predicates of different arities are considered different.
Documentation Convention: |
`f/N` |
≈ |
*relation `f` takes `N`-many arguments* |
# Modus Ponens — Computation ≈ Deduction
The logical rule \(p ∧ (p q) \;\; q\) says if we have \(p\), and from
that we know we can get a \(q\), then we have a \(q\). From the following program
on the left, we get `q(a)` is true.
p(a).
q(X) :- p(X).
We *rewrite* term `X` with atom `a` to obtain `q(a) :- p(a)` from the second rule,
but we know `p(a)`, and so we have *computed* the new fact `q(a)` by using the
deduction rule modus ponens.
# Conjunction ≈ Constraints — Disjunction ≈ Alternatives
Conjunction: `p(X), q(X)` means “let `X` be *a* solution to `p`, then use it in query `q`.”
Operational semantics: Let `X` be the first solution declared, found,
for `p`, in the user's script, then try `q`; if it fails, then *backtrack*
and pick the next declared solution to `p`, if any, and repeat until `q`
succeeds —if possible, otherwise fail.
yum(pie).
yum(apples).
yum(maths).
% ?- yum(Y), writeln(Y), fail.
% pie apples maths false.
“Fail driven loop” `p(X), print(X), fail.` gets a solution to `p`, prints
it, then fails thereby necessitating a backtrack to obtain a
different solution `X` for `p`, then repeats. In essence, this is prints
all solutions to `p`.
“Let Clauses”: Provided `X` is a fresh variable,
A Prolog program is the conjunction of all its clauses, alternatives ‘;’.
% (head body) ∧ (head body)
head :- body.
head :- body.
≈
% head body ∨ body
head :- body ; body.
Read ‘’ as ‘≥’, and ‘∨’ as maximum, then the following is the
“characterisation of least upper bounds”.
|
\((p q) ∧ (p r)\) |
≡ |
|
|
\(p (q ∨ p)\) |
“And binds stronger than Or”: `a,b;c ≈ (a,b);c`.
# [Unification](http://cs.union.edu/~striegnk/learn-prolog-now/html/node15.html)
A program can be written by having nested patterns, terms, then we use
matching to pull out the information we want!
Two terms *match* or *unify*, if they are equal or if they contain variables that
can be instantiated in such a way that the resulting terms are equal.
- **Unification:** Can the given terms be made to represent the same structure?
- This is how type inference is made to work in all languages.
- **Backtracking:** When a choice in unification causes it to fail, go back to the
most recent choice point and select the next available choice.
- Nullary built-in predicate `fail` always fails as a goal and causes backtracking.
## Operational Semantics
The unification predicate is `=/2`. It can be written with the usual
notation `=(L, R)` but can also be written infix `L = R`.
% Query: Who is loved by Jay?
?- loves(jay, X) = loves(jay, kathy).
% X = kathy
Operationally ` = ` behaves as follows:
1. If either is an unbound variable, assign it to the other one.
- A constant unifies only with itself.
- A variable unifies with anything.
2. Otherwise, they are both terms.
- Suppose \( ≈ f(e,…,e)\) and \( ≈ g(d,…,d)\).
- If `f` is different from `g`, or `n` different from `m`, then crash.
- Recursively perform `e = d`.
Ensure the variable instantiations are compatible in that a
variable is associated with at most one value —which is
not true in `f(1,2) = f(X,X).`
**Thus variables are single ‘assignment’!** |
Exception! Each occurrence of the anonymous variable `_`
is independent: Each is bound to something different.
3. If two terms can't be shown to match using the above clauses,
then they don't match.
*Unification lets us solve equations!* It lets us **compute!** |
## 'symbol' = symbol
The query `'symbol' = symbol` is true since both are considered to be the same
atom. Whereas `'2' = 2` is false since `'2'` is a symbolic atom but `2` is a number.
The *discrepancy predicate* `\=/2` succeeds when its arguments don't unify;
e.g., `'5' \= 5` is true.
## Unification performs no simplification, whence no arithmetic
Unification performs no simplification, whence no arithmetic.
This means, for example, we can form pairs by sticking an infix operator between two items; moreover we can form distinct kinds of pairs by using different operators.
?- C + "nice" = woah + Z.
C = woah, Z = "nice".
% ‘+’ and ‘/’ are different,
% so no way to make these equal.
?- C + "nice" = woah / Z.
false.
# Algebraic Datatypes
Uniform treatment of all datatypes as predicates! Enumerations, pairs, recursives:
Haskell
data Person = Me | You | Them
data Pair a b = MkPair a b
data Nat = Zero | Succ Nat
sum Zero n = n
sum (Succ m) n = Succ (sum m n)
Prolog
person(me).
person(you).
person(them).
pair(_, _).
nat(zero).
nat(succ(N)) :- nat(N).
sum(zero, N, N).
sum(succ(M), N, succ(S))
:- sum(M, N, S).
Exercise: Form binary trees.
# Arithmetic with `is` —Using Modules
Use `is` to perform arithmetic with `+, -, *, /, **, mod`, and
`//` for integer division.
% How do we make this equation equal?
?- X = 3 + 2.
% X = 3 + 2; this choice of variables make its equal!
% Everything is a term! Terms don't ‘compute’!
?- +(3, 2) = 3 + 2. % true
?- +(3, 2) = 6 - 1. % false
?- X is 3 + 2. % X = 5
?- 5 is 6 - 1. % true
?- 5 is X. % CRASH!
?- 3 + 2 is 6 - 1. % CRASH!
?- +(3, 2) =:= 6 - 1. % true
?- 1 =:= sin(pi/2). % true
?- X =:= 3 + 2. % CRASH!
?- X = 2, Y = 3, X + Y =:= 5. % true
- `is` takes a *variable, or a numeric constant,* and an arithmetical
expression as arguments.
- `L is R` means “ unify `L` with the result of simplifying `R` ”
- If `R` mentions an unbound variable, crash!
- `=:=` has both arguments as *concrete terms*, it evaluates them and compares the results.
` =:= ` |
≈ |
`L is , R is , L = R`. |
## Using Modules
The [Constraint Logic Programming over Finite Domains](http://www.swi-prolog.org/pldoc/man?section=clpfd) library provides a number of
useful functions, such as `all_distinct` for checking a list has unique elements.
See [here](http://www.swi-prolog.org/pldoc/man?section=clpfd-sudoku) for a terse solution to Sudoku.
In particular, `=:=` is too low level —e.g., it d ... ...
近期下载者:
相关文件:
收藏者: