|
FirstOrderTerm.java
|
// FILE. . . . . d:/hak/hlt/src/hlt/fot/FirstOrderTerm.java // EDIT BY . . . Hassan Ait-Kaci // ON MACHINE. . Hak-Laptop // STARTED ON. . Sat Jul 14 07:23:41 2018 package hlt.fot;
This is an interface for first-order terms defined on a signature of
Functors. It is either
implemented by a FirstOrderTermStructure
(which uses a signature of objects of class Functor) and as a Variable).
|
import java.util.Stack; import java.util.HashMap; import java.util.ArrayList; import java.util.Iterator; public interface FirstOrderTerm { /* ************************************************************************ */ // To be implemented by instantiating classes: /* ************************************************************************ */
| Returns true iff this is a Variable. |
public boolean isVariable ();
| Returns a term that is equal to this term after having all dereferencing of its contents. |
public FirstOrderTerm deref ();
| Returns a String value for this term taking all its variable bindings into account. This provides a simple default implementation which is overridden in the classes implementing this class (Variable and FirstOrderTermStructure) to prevent it from building a new term explicitly each time its string form is wanted (as this default does). |
default public String derefToString () { return deref().toString(); }
| Returns true is this term is equal symbol for symbol to the given one (although they may be different individuals). |
public boolean equal (FirstOrderTerm term); /* ************************************************************************ */ // Static structures and methods: /* ************************************************************************ */ /* ************************************************************************ */ // Lattice operations: /* ************************************************************************ */
| UNIFICATION |
static Stack unifyStack = new Stack();
| Unify the given pair of first-order terms and return true iff they are unifiable. This will possibly bind variables that occur in either term. |
public static boolean unify (FirstOrderTerm lhs, FirstOrderTerm rhs) { unifyStack.clear(); unifyStack.push(lhs); unifyStack.push(rhs); boolean unifiable = true; while (unifiable && !unifyStack.isEmpty()) { lhs = (FirstOrderTerm)unifyStack.pop(); rhs = (FirstOrderTerm)unifyStack.pop(); if (lhs.isVariable()) lhs = ((Variable)lhs).deref(); if (rhs.isVariable()) rhs = ((Variable)rhs).deref(); if (lhs == rhs) continue; if (lhs.isVariable()) { Variable V = ((Variable)lhs); if (V.occursIn(rhs)) unifiable = false; else V.bind(rhs); continue; } if (rhs.isVariable()) { Variable V = ((Variable)rhs); if (V.occursIn(lhs)) unifiable = false; else V.bind(lhs); continue; } // both are structures: FirstOrderTermStructure L = (FirstOrderTermStructure)lhs; FirstOrderTermStructure R = (FirstOrderTermStructure)rhs; if (L.functor().equal(R.functor())) for (int i=1; i <= L.functor.arity(); i++) { unifyStack.push(L.argument(i)); unifyStack.push(R.argument(i)); } else unifiable = false; } return unifiable; } /* ************************************************************************ */
| GENERALIZATION |
| The generated generalizing variables. |
public static ArrayList generatedVariables = new ArrayList();
| The substitution mapping generated variables to the subterms of the generalized lhs. |
public static HashMap lSubstitution = new HashMap();
| The substitution mapping generated variables to the subterms of the generalized rhs. |
public static HashMap rSubstitution = new HashMap();
| Clears all substitutions and generated variables. |
public static void resetGeneralizer () { generatedVariables.clear(); lSubstitution.clear(); rSubstitution.clear(); }
| Unapplying the current left and right substitutions to the given terms, and returning a pair of terms. |
private static FirstOrderTermPair unapply (FirstOrderTerm lhs, FirstOrderTerm rhs) { Variable V; FirstOrderTerm L; FirstOrderTerm R; for (int i = 0; i < generatedVariables.size(); i++) { V = (Variable)generatedVariables.get(i); L = (FirstOrderTerm)lSubstitution.get(V); R = (FirstOrderTerm)rSubstitution.get(V); if (lhs.equal(L) && rhs.equal(R)) return new FirstOrderTermPair(V,V); } return new FirstOrderTermPair(lhs,rhs); }
| This returns the term generalizing the given pair of terms. It proceed recursively on pairs structures with equal-functors. As it proceeds it simultaneously builds up the left and right generalizing substitutions as needed. |
public static FirstOrderTerm generalize (FirstOrderTerm lhs, FirstOrderTerm rhs) { // Equal Variables if (lhs.isVariable() && lhs == rhs) return lhs; // Variable-Term: if ((lhs.isVariable() || rhs.isVariable()) && !lhs.equal(rhs)) { Variable newVariable = Variable.anonymousVariable(); lSubstitution.put(newVariable,lhs); rSubstitution.put(newVariable,rhs); generatedVariables.add(newVariable); return newVariable; } FirstOrderTermStructure L = (FirstOrderTermStructure)lhs; FirstOrderTermStructure R = (FirstOrderTermStructure)rhs; // Unequal Functors: if (!L.functor().equal(R.functor())) { Variable newVariable = Variable.anonymousVariable(); lSubstitution.put(newVariable,lhs); rSubstitution.put(newVariable,rhs); generatedVariables.add(newVariable); return newVariable; } // Equal Functors: Functor F = L.functor(); int N = F.arity(); FirstOrderTermStructure newStructure = N==0 ? new FirstOrderTermStructure(F) : new FirstOrderTermStructure(F,new FirstOrderTerm[N]); for (int i = 1; i <= N; i++) { FirstOrderTermPair P = unapply(L.argument(i),R.argument(i)); newStructure.setArgument(i,generalize(P.left(),P.right())); } return newStructure; } }
This file was generated on Sat Aug 25 07:59:54 CEST 2018 from file FirstOrderTerm.java
by the hlt.language.tools.Hilite Java tool written by Hassan Aït-Kaci