Justification Trees

Reading a justification tree

Prolog makes this initial step easy. Given a source file $Src$, load the JSON as a dictionary.

read_json_dict(Src, Dict) :-
    setup_call_cleanup(open(Src, read, Stream),
                       json_read_dict(Stream, Dict),
                       close(Stream)).

The source will not be just a tree. It will be a set of justification trees: one tree for each query.

Walking the tree using a DCG

A tree is a recursive structure of nodes with sub-node children. What do justification trees look like when rendered in JSON? Dictionary objects with a list of sub-dictionary children—in a nutshell. See $Tree$ in Figure 1.

A basic tree walk can become a definite-clause grammar (DCG) where the tree or sub-tree is an argument, and its difference list becomes a list of Graphviz directives.

json_dot(Dict, Options) -->
    answers_dot(Dict.answers, Options_).

answers_dot(Answers, Options) -->
    sequence(answer_dot(Options), Answers).

answer_dot(Options, Answer) -->
    answer_tree_dot(Answer.tree, Options).

answer_tree_dot(_{node:Node, children:Children}, Options) -->
    { value_term(Node.value, query)
    },
    sequence(answer_tree_query_dot(Options), Children).

answer_tree_query_dot(Options, Answer) -->
    sequence(answer_tree_query_dot(Options), Answer.children).

Each answer is a dictionary of pairs. Every dictionary answer has:

• an answer counter;
• a sub-dictionary of bindings;
• a sub-dictionary of constraints;
• a list of model terms;
• a justification tree; and
• a time.

The top level of each answer has a node atom value of query. It acts as a root node. The children of the root node constitute its justifications.

Node values to Prolog terms

Every node has a value. See Figure 1, $Node$ class.

Node values take the form of a dictionary after loading the JSON. The JSON becomes a Prolog dictionary of dictionaries and lists of dictionaries.

See the implementation below. It recursively constructs a $Term$ given a node’s $Value$ dictionary. Mapping the arguments using itself leads to recursion. This implies that each argument could itself map to a sub-compound. The logic allows for this.

%!  value_term(+Value:dict, ?Term) is semidet.

value_term(Value, Term), is_dict(Value) => dict_term(Value, Term).
value_term(Value, List), is_list(Value) => maplist(value_term, Value, List).

dict_term(Value, Var), _{type:"var",
                         name:Var} :< Value => true.
dict_term(Value, Atom), _{type:"atom",
                          value:String} :< Value => atom_string(Atom, String).
dict_term(Value, Value), _{type:"number",
                           value:Value} :< Value => true.
dict_term(Value, Rational), _{type:"rational",
                              numerator:Numerator,
                              denominator:Denominator} :< Value =>
    rational(Rational, Numerator, Denominator).
dict_term(Value, Term), _{type:"compound",
                          functor:Functor,
                          args:Args} :< Value =>
    atom_string(Functor_, Functor),
    maplist(value_term, Args, Args_),
    Term =.. [Functor_|Args_].

The value_term/2 predicate converts a Prolog dictionary (parsed from JSON) that represents a term into an actual Prolog term. The predicate deals with cases where the dictionary represents different types of terms, such as variables, atoms, numbers, rational numbers, and compound terms. It recursively processes the arguments of compound terms to construct the final term. The predicate handles the following cases:

• If the input is a dictionary representing a variable, it extracts the variable name and returns it as a Prolog string.
• If the dictionary represents an atom, it converts the string value to a Prolog atom.
• If the dictionary represents a number, it returns the number as is.
• If the dictionary represents a rational number, it constructs a rational term from the numerator and denominator.
• If the input is a dictionary representing a compound term, it recursively processes the arguments and constructs the compound term using the functor and the arguments.

The predicate employs dictionary pattern matching (:<) to safely extract the relevant fields from the dictionary, and for clarity. It handles nested compounds by recursively mapping the arguments to value terms. The predicate is semi-deterministic, meaning it succeeds at most once; if the input dictionary does not match any of the expected patterns, it fails silently. This allows for safe handling of the JSON structure without raising exceptions for unexpected formats.

The implementation assumes that the JSON structure follows a specific format, where each term is represented as a dictionary with a type field indicating whether it is a variable, atom, number, rational, or compound. If the JSON structure changes or new term types are added, the predicate will require updating.

The value_term/2 predicate is used to convert the JSON representation of terms into Prolog terms, which can then be used in further processing or output—particularly useful in the context of generating a DOT graph from a JSON source produced by s(CASP), where terms represent nodes in the justification tree. It is a crucial part of justification tree processing, allowing the conversion of JSON representations of terms into Prolog terms that can be used to construct the graph structure, and designed to be used in conjunction with the dict_term/2 helper predicate, which handles the conversion of a Prolog dictionary (parsed from JSON) into a Prolog term. The dict_term/2 predicate is responsible for converting the dictionary representation of terms into actual Prolog terms.

Printing message lines

The scasp_just_dot module at GitHub adds node and edge styling; true edges receive a solid dark green edge while “likely” edges render as dotted dark green; similarly, false edges render as dark red while unlikely as dotted dark red. The underlying DCG generates “message lines” for use by print_message_lines/3.