Decision trees

The pattern matching algorithm uses decision trees. These decision trees are attached to symbols and can be inspected for debugging purposes. To print the decision tree of a symbol s of a module whose module path is M (see Module path), its decision tree may be printed with

lambdapi decision-tree M.s

The package configuration file of module M must be above the current working directory (closer to the root of the file system), or in the same directory.

The decision trees are printed to the standard output in the dot language. A dot file tree.gv can be converted to a png image using dot -Tpng tree.gv > tree.png. The one-liner

lambdapi decision-tree M.s | dot -Tpng | display

displays the decision tree of symbol M.s (display is part of imagemagick). For other output formats, see graphviz documentation.

Description of the generated graphs

Decision trees are interpreted during evaluation of terms to get the correct rule to apply. A node is thus an instruction for the evaluation algorithm. There are labeled nodes, labeled edges and leaves.

  • Circle represent regular nodes. Let n be the label of the node, the next node is reached by performing an atomic match between the n th term of the stack and the labels of the edges between the node and its children. Let t be the term taken from the stack and matched against the labels. The labels of the edges can be

    • s_n, the atomic match succeeds if t is the symbol s applied to n arguments, the n arguments are put back in the stack;

    • λvn, the atomic match succeeds if t is an abstraction. the body is substituted with (fresh) variable vn. Both the domain of the abstraction and the substituted body are put back into the stack;

    • Πvn, the atomic match succeeds if t is a product. The body is substituted with a (fresh) variable vn. Both the domain of the product and the substituted body are put back into the stack

    • *, the atomic match succeeds whatever t is.

  • Rectangles represent storage nodes. They behave like regular nodes, except that the term of the stack is saved for later use.

  • Diamonds represent condition nodes. The next node is reached by performing a condition check on terms that have been saved. If the condition is validated, the ✓-labeled edge is followed, and the ✗-labeled one is followed otherwise. The label of the nodes indicates the condition, it can be

    • n ≡ m which succeeds if the nth and mth saved terms are convertible,

    • xs ⊆ FV(n) which succeeds if the free variables of the nth saved term is a superset of the free variables xs.

  • Triangles represent stack check nodes. The next node is the left child if the stack of arguments is empty, the right child otherwise. These nodes can only appear in trees built for sequential symbols.

Note for developers: the decision tree of ghost symbols can be printed as well using the --ghost flag. For instance,

lambdapi decision-tree --ghost M.≡