SWI-Prolog Did You Know Did you know? SWI-Prolog supports TIPC Search Documentation:
The Byrd Box Model And Ports

2.10.1 The Byrd Box Model And Ports

Standard Prolog debugging tools are built around the so-called "Byrd Box Model" or "4 Port Model" which models each predicate in a Prolog program as a state machine ("box") that transitions through states ("ports") as a program is evaluated. The developer can ask the engine to pause for program inspection when it reaches specific ports or predicates.

As we go through this overview, remember that a "port" is just another word for a "state" in the state machine that each predicate transitions through during evaluation. The state machine is called a "box" because it is drawn like this: 

                *--------------------------------------*
         Call   |                                      |   Exit
     ---------> +  descendant(X,Y) :- offspring(X,Y).  + --------->
                |                                      |
                |  descendant(X,Z) :-                  |
     <--------- +     offspring(X,Y), descendant(Y,Z). + <---------
         Fail   |                                      |   Redo
                *--------------------------------------*

The standard ports are: call, redo, exit and fail. SWI-Prolog extends this with two more: unify and exception. Each trace happens at a particular phase of predicate resolution. Recall that when resolving or "proving" a predicate, the Prolog engine:

  1. Collects all rules that might match by having a head with the same name and number of arguments

    • call is traced, once, if any rules might match.
    • redo is also traced when the engine backtracks to find the next matching rule.

  2. Finds the next matching rule whose head can be unified with the predicate

    • unify is traced with the results of unification if one is found.
    • fail is traced if no rule heads can be unified.

  3. Applies variable assignments from unification to clauses in the rule body and continues at #1 with the updated clauses
  4. After all of the body clauses of the matched rule have either succeeded, failed, or thrown an exception:

    • exit is traced if all of them succeeded (meaning this rule is true).
    • fail is traced if any of them failed (meaning this rule is false).
    • exception is traced if any of them threw an exception.

    This means there can be a lot of traces between the initial call and the end of tracing for a particular predicate.

Tags are associated to your profile if you are logged in|Report abuse
Tags:
  • doc-needs-help
LogicalCaptain said (2020-12-04T08:51:11):0 upvotes 0 0 downvotes
Picture of user LogicalCaptain.

Needs correction

"which models each predicate in a Prolog program as a state machine ("box") that transitions through states ("ports") as a program is evaluated."

should be corrected to

"which models each predicate activation in a Prolog program as a state machine ("box") that transitions through states ("ports") as a program is evaluated."

The same predicate can have multiple predicate activations (which are stack frames) going, and inside a Byrd box, there are other Byrd boxes, all the way down.

This makes the Byrd box model actually a bit hard to understand. It also skips about the details concerning what happens at the head of a predicate, and at tail end of a clause.

The "choice point model" whereby proof search is modeled as a tree that is growing or shrinking is easier on the mind.

The ports are also rather "events" that the debugger can listen for rather than "states". The model just progresses through the ports.

Companion info

My notes on the Byrd Box model here

Check out the research report Une sémantique observationnelle du modèle des boîtes pour la résolution de programmes logiques (version étendue) (in french) for a ton of Byrd Box images and their link to proof trees.

As with so much of the Prolog world, historical floatsam is carried along: The "Exit" port should have been called the "Succ" port from the very beginning. Everybody should really name it that way.

DETERMINISTIC PREDICATE
(well-behaved: closing off the REDO port, i.e. "leaving no choicepoint")
       
             +---------------------+
     -------⊳|Call------⊳-----⊳Succ|------⊳
   from      |                     |      to
   prev      |                     |      next
   pred      |                     |      pred
     ⊲---+   |Fail             Redo|   +---
         |   +---------------------+   |
         |                             |
         +---⊲----no choicepoint----⊲--+

SEMI-DETERMINISTIC PREDICATE
(well-behaved: closing off the REDO port, i.e. "leaving no choicepoint")
              
             +---------------------+
     -------⊳|Call---+--⊳-----⊳Succ|------⊳
   from      |       |             |      to
   prev      |       ∇             |      next
   pred      |       |             |      pred
     ⊲---+---|Fail⊲--+             |   +---
         |   +---------------------+   |
         |                             |
         +---⊲----no choicepoint----⊲--+

NONDETERMINISTIC PREDICATE (succeeds maybe 0 times)
MULTI PREDICATE (succeeds at least once)
(well-behaved if it closes off the REDO port at the last solution, i.e. "leaves no choicepoint")
              
             +---------------------+
     -------⊳|Call---+--⊳--+--⊳Succ|------⊳
   from      |       |     |       |      to
   prev      |       ∇     ∆       |      next
   pred      |       |     |       |      pred
     ⊲---+---|Fail⊲--+--⊲--+---Redo|⊲--+---
         |   +---------------------+   |
         |                             |
         +---⊲----no choicepoint----⊲--+