Held: Monday, April 17, 2006
Summary:
Today we begin to explore predicate logic programming,
one of the standard models of declarative programmming.
Related Pages:
Assignments
Notes:
- Are there questions on the exam?
- Don't count on homework getting graded.
Overview:
- Declarative Programming, Revisited.
- Predicate Logic.
- Predicate Logic Programming.
- As I've suggested in the past, declarative programming is a
paradigm in which we focus on the what of an algorithm
(that is, the relationship between data) rather than the
how.
- As Kowalski suggests, we can also think about both, but we should
think about them separately (at least at first pass).
- To Kowalski (and to many), thinking about what involves some
formal system of logic.
- Predicate logic is the most common.
- There are others, such as equational logic.
- One of the most common(?) logics is predicate logic, a
logic based on the definition and understanding of predicates,
functions that return true or false.
- What are some typical predicates? It depends on the domain, but here
are some that we'll probably visit.
- X
is an ancestor of
Y.
- L
is a sorted list
.
- S
is a sorted version of
L.
- X
is a person
.
- X
is mortal
.
- How do we define predicates?
- One way is by listing membership (as in SQL).
- More Traditionally, using some standard operations, including
- if-then, if-and-only-if
- and, or, not
- for each (with corresponding variables)
- there exists (with corresponding variables)
- As with functions, we might also list truthful statements.
- For example,
- For all X, if X is a person then X is mortal. (Phrased in
ancient times as "all men are mortal".)
- Socrates is a mortal.
- How might we write
is an ancestor of
?
- How might we use the predicate logic as a programming language?
- We could state "theorems" and ask the system to prove the theorems
based on the rules of predicate logic and the definitions contained
within our program. In effect, we state our theorem as a question and
ask the program to answer it.
- For example: "Is Socrates mortal?" "Yes, because Socrates is
a person and all people are mortal."
- Similarly: "Are there any mortals?" "Yes, Socrates is a mortal
because Socrates is a person and all people are mortal."
- Similarly: "Is Socrates immortal?" "No, because Socrates is
mortal (see above) and no mortal is immortal."
- And "Is Lou Reed influential?" "Yes, because Lou Reed was a
member of the Velvet Underground and R.E.M. were influenced by the
Velvet Underground."
- How might we implement such a language? Well, there are two
aspects, depending on the type of question that is being asked.
- To prove a theorem about an atom. In this case, we might "plug" the
atom in to the right hand side and then attempt to prove the right
hand side.
- To prove a theorem about a variable, we may need to "guess" instantiations
and plug in.
- Note that the first quickly becomes the second. For example, in
proving that Lou Reed is influential, we need to identify a band that
Lou Reed was/is a member of. Then, we need to determine whether that
band is influential.
- It turns out that some aspects of such proofs are extremely difficult.
In particular, it may be impossible to prove a negation.
- To simplify matters, we may want to write a disjunction of
Horn clauses: clauses that define predicates in which consist
of only an and of assertions (i.e., no nots, the only ors are
used around our Horn clauses).
- Top-down: Pick a clause left to prove, pick a rule that defines the clause, replace clause by rhs.
- Bottom-up: Pick a proven clause. Pick a rule that is fully proven on the rhs. Build a new proven clause.
- Parallel: Either can be done in parallel.
- Logic can affect control. Consider Kowalski's example.
;
Check with Bobby