#include "unify.h"

Contents

• Public Routines
• Public Definitions
• Introduction

Public Routines in File unify.c

Index

Details

Term apply(Term t, Context c);

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

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

Plist context_to_pairs(Ilist varnums, Context c);

BOOL empty_substitution(Context s);

void fprint_context(FILE *fp, Context c);

void fprint_trail(FILE *fp, Trail t);

void fprint_unify_mem(FILE *fp, BOOL heading);

void free_context(Context p);

Context get_context(void);

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

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

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

void p_context(Context c);

void p_trail(Trail t);

void p_unify_mem();

BOOL subst_changes_term(Term t, Context c);

void undo_subst(Trail tr);

void undo_subst_2(Trail tr, Trail sub_tr);

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

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);

Ilist vars_in_trail(Trail tr);

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

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.)