Declarative programming: facts, rules and goals
| English |
|---|
| fact/fækt/ |
| declarative programming/dɪˈklærətɪv ˈprəʊɡræmɪŋ/ |
| rule/ruːl/ |
| goal/ɡəʊl/ |
| backtrack/ˈbæktræk/ |
| unification/ˌjuːnɪfɪˈkeɪʃn/ |
Ask who can borrow a camera
- A media club keeps facts about its members and completed training. It wants to ask who can borrow a camera without writing a new loop for every question.
- Declarative programming 声明式编程 describes facts, rules and a goal 目标. A logic engine searches for values that make the goal true. The programmer still has to write correct rules; the engine does not read minds or club noticeboards.
Facts state what is known
- A fact 事实 is an assertion in the knowledge base. In
member(aya)., the predicatememberrelates one person to club membership.trained(aya, camera).relates a person to a piece of equipment. - This lesson uses Prolog-style notation: lowercase names are constants or predicates; uppercase names are variables. A full stop ends each fact or rule.
member(aya).
member(ben).
member(chen).
trained(aya, camera).
trained(chen, camera).
trained(ben, audio).
Given the facts member(ben). and trained(ben, audio)., which statement below is a supplied fact?
member(ben). is given directly. The knowledge base does not include camera training for Ben.
A rule combines conditions
- A rule 规则 states when a conclusion holds. Read
:-as “if” and the comma as AND: a person may borrow a camera if they are a member and have camera training. Personnames the same variable in all three places. The engine must find one value that satisfies both conditions, not one member and a different trained person.
can_borrow(Person, camera) :- member(Person), trained(Person, camera).
In the rule can_borrow(Person, camera) :- member(Person), trained(Person, camera)., the comma between the two conditions means ____.
Both membership and camera training must hold for the same Person.
A goal asks a question
- The goal
?- can_borrow(aya, camera).asks for a yes/no result. The engine matches the rule and checksmember(aya)andtrained(aya, camera): both facts exist, so the goal succeeds. - The goal
?- can_borrow(Person, camera).asks for bindings of the variable. With this knowledge base, the answers arePerson = ayaandPerson = chen. These are goals to reason about; the displayed blocks are notation, not a runnable playground.
Club members are aya, ben and chen. Aya and Chen are camera-trained; Ben is audio-trained only. The rule can_borrow(Person, camera) requires both membership and camera training. Who satisfies can_borrow(Person, camera)?
Aya and Chen have both required facts. Ben has audio training only.
The Person variable in member(Person) may have a different value from Person in trained(Person, camera) during one proof.
All occurrences of the same variable must keep the same binding in that proof.
Worked example: trace a failed candidate
- Start with
Person = ben.member(ben)succeeds.trained(ben, camera)fails: the available training fact is for audio, which does not match camera. - The engine backtracks 回溯 to try another candidate,
Person = chen. Both conditions succeed. If more answers are requested, it continues searching; if no candidates remain, there are no more answers.
Trace the remaining search after Aya has already been returned.
Ben is a member but lacks a matching camera-training fact; the engine then tries Chen.
Matching shares values across a rule
- Unification 合一 matches terms while consistently binding variables. Matching
trained(Person, camera)withtrained(chen, camera)bindsPersontochen; matching it withtrained(ben, audio)fails because the equipment differs. - A failed goal means it cannot be proved from these facts and rules. It does not prove that Ben has never used a camera in real life; the knowledge base may simply be incomplete.
Matching trained(Person, camera) with trained(chen, camera) binds Person to ____.
The equipment matches and the first argument provides the binding chen.
Worked example: write a new rule
- Requirement: a mentor can help someone only when the mentor has camera training and the learner is a member. Add the rule below, then ask
?- can_help(aya, ben).. trained(aya, camera)andmember(ben)both exist, so the goal succeeds. This rule allows Aya to help herself too. If self-help must be excluded, the requirement needs another condition; do not invent it silently.
can_help(Mentor, Learner) :- trained(Mentor, camera), member(Learner).
Given trained(aya, camera). and member(ben)., and the rule can_help(Mentor, Learner) :- trained(Mentor, camera), member(Learner)., does can_help(aya, ben) succeed?
Aya has camera training and Ben is a member; Ben need not have camera training to be a learner.
Marks that slip away
- A fact states something known; a rule derives a conclusion when its conditions hold; a goal asks whether a conclusion can be proved or which values make it true.
- Keep repeated variables consistent.
member(X), trained(Y, camera)would let an untrained member qualify because someone else has training. Changing a variable name can change the rule's meaning.
From a requirement to a proof
- Write facts, translate each requirement into a rule, and pose a goal. Trace each variable binding through every condition and try alternatives when a candidate fails.
- Here only Aya and Chen may borrow a camera. Ben's audio training is not camera training. Results follow from the supplied knowledge base, not a guess about real people.
Club members are aya, ben and chen. Aya and Chen are camera-trained; Ben is audio-trained only. The rule can_borrow(Person, camera) requires both membership and camera training. How many people satisfy can_borrow(Person, camera)?
Aya and Chen are the two solutions.
A failed goal proves the corresponding event never happened outside this knowledge base.
Failure means the goal cannot be proved from the available facts and rules.