# #include "unify.h"

This page has information from files unify.h and unify.c.

## Contents

- Public Routines
- Public Definitions
- Introduction

## Public Routines in File unify.c

#### Index

apply | fprint_trail | occur_check | undo_subst_2
apply_substitute | fprint_unify_mem | p_context | unify
apply_substitute2 | free_context | p_trail | variable_substitution
context_to_pairs | get_context | p_unify_mem | variant
empty_substitution | match | subst_changes_term | vars_in_trail
fprint_context | match_weight | undo_subst |

#### Details

    Term apply(Term t, Context c);

This routine applies the substitution in Context c to Term t. See the explanation of unify() for an example of the use of apply().

    Term apply_substitute(Term t, Term beta, Context c_from,
    		      Term into_term, Context c_into);

This routine is like apply(), but when it reaches a particular subterm (into_term) of the source term (t), it continues with another source term (beta). This routine is intended to be used for paramodulation, to avoid unnecessary work. For example, when paramodulating alpha=beta into p[into_term], where alpha unifies with into_term, we construct the appropriate instance of p[beta] in one step by using this routine.

    Term apply_substitute2(Term t, Term beta, Context c_from,
    		       Ilist into_pos, Context c_into);

Similar to apply_substitute, but the into_term is specified with a position vector instead of the term itself. This is so that the into term can be a variable. (Recall that variables are probably shared, and we have to specify an *occurrence*.)

    Plist context_to_pairs(Ilist varnums, Context c);

    BOOL empty_substitution(Context s);

    void fprint_context(FILE *fp, Context c);

This routine prints (to FILE *fp) a Context.

    void fprint_trail(FILE *fp, Trail t);

This routine prints (to FILE *fp) a Trail. The whole list is printed.

    void fprint_unify_mem(FILE *fp, BOOL heading);

This routine prints (to FILE *fp) memory usage statistics for data types associated with the unify package. The Boolean argument heading tells whether to print a heading on the table.

    void free_context(Context p);

    Context get_context(void);

    BOOL match(Term t1, Context c1, Term t2, Trail *trp);

This routine checks if Term t2 (without a Context) is an instance of Term t1 (in Context c1). If successful, Context c1 and Trail * trp are updated. The calling sequence and the use of Contexts and Trails is similar to those for unify().

    BOOL match_weight(Term t1, Context c1, Term t2, Trail *trp, int var_sn);

Special-purpose match for weighting.

    BOOL occur_check(int vn, Context vc, Term t, Context c);

This function checks if a variable with index vn (in Context vc) occurs in Term t (in Context c), including the top case, where t is the variable in question.

    void p_context(Context c);

This routine prints (to stdout) a Context.

    void p_trail(Trail t);

This routine prints (to stdout) a Trail. The whole list is printed.

    void p_unify_mem();

This routine prints (to stdout) memory usage statistics for data types associated with the unify package.

    BOOL subst_changes_term(Term t, Context c);

This routine checks if a subsitution would change a term, if applied.

    void undo_subst(Trail tr);

This routine clears substitution entries recoded in Trail tr, and frees the corresponding Trail nodes.

    void undo_subst_2(Trail tr, Trail sub_tr);

It is assumed that Trail sub_tr is a subtrail of Trail tr. This routine clears part (maybe all) of a substitution, by clearing the entries from tr up to, but not including sub_tr. The corresponding Trail nodes are deallocated, so the caller should no longer refer to tr. (This is useful for inference rules like hyperresolution, which backtrack, undoing parts of substitutions.)

    BOOL unify(Term t1, Context c1,
    	   Term t2, Context c2, Trail *trp);

This routine tries to unify two terms in their respective contexts. Trail * trp is the address of a Trail. If successful, the trail is extended (at its front) with substitutions that were made, and trp is updated to point to the new beginning of the trail. If unify fails, the Contexts and the Trail * are not changed.

You must make sure, before calling unify(), that no variable v in t1 or t2 has VARNUM(v) >= MAXVARS. This is usually accomplished by calling a routine that renames variables.

Here is an example how to use unify(), apply(), and undo_subst(). Assume we have terms t1 and t2. (Terms t1 and t2 may share variables, but we "separate" the variables by using different contexts. That is, variable v1 in context c1 is different from variable v1 in context c2.)

        {
            Context c1 = get_context();
            Context c2 = get_context();
            Trail tr = NULL;
            if (unify(t1, c1, t2, c2, &tr)) {
                Term t3 = apply(t1, c1);
                Term t4 = apply(t2, c2);
                if (term_ident(t3, t4))
                    printf("everything is OK\n");
                else
                    printf("something is broken\n");
                undo_subst(tr);
                zap_term(t3);
                zap_term(t4);
            }
            else
                printf("unify fails\n");
            free_context(c1);
            free_context(c2);
        }

    BOOL variable_substitution(Context s);

    BOOL variant(Term t1, Context c1,
    	    Term t2, Trail *trp);

This routine checks if Term t1 (in Context c1) and Term t2 (without a Context) are variants, that is, if each is an instance of the other. If successful, the unifying substitution is in Context c1. The calling sequence and the use of Contexts and Trails is the same as for unify().

    Ilist vars_in_trail(Trail tr);

Return the list of variables (as integers) in a trail. Note that this ignores the contexts associated with the varibles.

## Public Definitions in File unify.h

    /* Dereference a variable. */

    #define DEREFERENCE(t, c) { int i; \
        while (c!=NULL && VARIABLE(t) && c->terms[i=VARNUM(t)]) \
        { t = c->terms[i]; c = c->contexts[i]; } }

    /* A Context records a substitution of terms for variables. */

    typedef struct context * Context;

    struct context {
      Term    terms[MAX_VARS];    /* terms substituted for variables */
      Context contexts[MAX_VARS]; /* Contexts corresponding to terms */
      int     multiplier;         /* for getting separate vars in apply */
      Term    partial_term;       /* for AC matching */
    };

    typedef struct trail * Trail;

    /* The following type is for backtrack unification and matching. */

    typedef enum { NO_ALT = 0,
    	       AC_ALT,
    	       COMM_ALT
                 } Unif_alternative;

## Introduction

This package handles ordinary unification and matching of terms. The methods are probably different from what you learned in your logic course, so pay close attention.

In situations where you consider instantiating the variables of a term t, you will have an associated Context c. The Context keeps track of the terms that are substituted for the variables--- think of it as a substitution table indexed by the variable number.

Contexts allow you to separate variables of two terms without creating a renamed copy of one of the terms. Say we have two terms with different Contexts: (t1,c1) and (t2,c2). If t1 and t2 share a variable, say v3, occurrences in t1 are a different variable from occurrences in t2, because the contexts are different. Think of the those variables as (v3,c1) and (v3,c2). In fact, when an instantiation is recorded in a Context, the variable in question is set to a pair, say (t4,c4) rather than just t4, because we have to know how to interpret the variables of t4.

There are situations where the terms being unified really do share variables, for example when factoring the literals of a clause; in those cases, you simply use the same context for both terms.

When you call unify(), match(), or any other routine that tries to make terms identical by instantiation, the terms you give are not changed---all of the action happens in their contexts (and in the trail, see below). So you do not have to copy terms before calling the routine.

When a unify or match routine succeeds, the Contexts are updated to reflect the common instance of the terms. Also, a Trail is returned. A Trail is a linked list of (variable,context) pairs telling exactly which variables were instantiated during the operation. Its purpose is to quickly restore the Contexts to their previous states.

You must explicitly allocate and free Contexts. To save time, we don't initialize the arrays each time a Context is re-allocated, and we don't check that Contexts are clear when they are freed. Therefore, you must make sure that a Context is clear before freeing it. See undo_subst(). Also, if you forget to clear the Context with undo_subst(), you will have a memory leak, because the Trail will be lost. (If you suspect that you have a bug which causes a non-empty context to be freed, you can enable a run-time check in free_context() and recompile unify.c.)

When you wish to find out what a context does to a term t, you can call apply(), which builds a new copy of the term with all of the instantiations of the context applied to the term t. But I wrote above that (v3,c1) is a different variable from (v3,c2)---what does apply do with uninstantiated variables? Each context has a unique multiplier (a small natural number); When apply() gets to an uninstantiated variable v, it returns a variable with index (multiplier*MAX_VARS)+VARNUM(v). Of course, this can give you VARNUMs > MAX_VARS, so you may have to rename variables of the result before calling a unification routine on the result.

Unification and matching can be used incrementally. For example, you can all unify() with a context which has entries from a previous call to unify(). Hyperresolution can be implemented by backtracking through the negative literals of a nucleus and the satellites that unify with a given literal of the nucleus, constructing and undoing partial substitutions along the way. Another example is subsumption. Checking whether one clause subsumes another can be done by incremental matching, backtracking through the literals of the potential subsumer, trying to map them to the literals of the other clause.

Associative-commutative unification and matching, and commutative unification and matching, use different unification code, because they have to deal with multiple unifiers for a pair of terms. (These other kinds of unification and matching may use the Context data type defined here.)