org.uacalc.terms
Class Taylor

java.lang.Object
  org.uacalc.terms.Taylor

public class Taylor
extends java.lang.Object

Let f be a k-ary operation symbol. We consider a set of equations where each side has the form f(x's and y's). For each index i there is at least one equation with the ith coordinate on the two sides are different (so f is a Taylor term).

We are looking to see if there is some term t in this language of f that is a Markovic-McKenzie-Siggers term. That is, an idempotent term satisfying
t(y,x,x,x) = t(x,x,y,y) and t(x,x,y,x) = t(x,y,x,x)
By idempotence every term in f can be assumed to have a balanced term tree. For depth d such a tree has k^d leaves and the term is determined by the vector of variables at the leaves. So terms of depth d can be represented by a vector of variables of length k^d and linearly ordered lexicographically.

We use the equations of f to effective rewrite this vector into the least equivalent one least in the lexicographic order. Using this we search all 4 variable terms for a MMS term.

Author:

ralph

Constructor Summary

Taylor(int arity, java.util.List<java.util.List<IntArray>> inteqs)

Taylor(OperationSymbol sym, java.util.List<java.util.List<IntArray>> inteqs)

Taylor(Term taylor, java.util.List<Equation> eqs)

Method Summary

int	arity()
IntArray	canonicalForm(IntArray arr)
Term	canonicalForm(Term t) Find the canonical form of a term t in the language of f with variables x and y.
java.util.List<Equation>	equations()
java.util.List<java.util.List<IntArray>>	inteqs()
Term	interprets(Taylor g, int level) Find a term which in the language of this which satisfies the identities of g.
static int	lexicographicallyCompare(int[] a, int[] b)
static int	lexicographicallyCompare(IntArray a, IntArray b)
int	lexicographicallyCompare(Term s, Term t)
static void	main(java.lang.String[] args)
Term	makeBalancedTayorTerm(OperationSymbol f, int depth, java.util.List<Variable> varList) Constructs a term with a balanced term tree.
static Taylor	markovicMcKenzieTerm()
static Taylor	siggersTerm()
Term	termFromArray(int[] arr)
Term	termFromArray(int[] arr, int start, int len)

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

Constructor Detail

Taylor

public Taylor(Term taylor,
              java.util.List<Equation> eqs)

Taylor

public Taylor(OperationSymbol sym,
              java.util.List<java.util.List<IntArray>> inteqs)

Taylor

public Taylor(int arity,
              java.util.List<java.util.List<IntArray>> inteqs)

Method Detail

canonicalForm

public Term canonicalForm(Term t)

Find the canonical form of a term t in the language of f with variables x and y. This first reduces via idempotence and then chooses the lexicographic order with x before y.

Parameters:

t -

Returns:

canonicalForm

public IntArray canonicalForm(IntArray arr)

markovicMcKenzieTerm

public static Taylor markovicMcKenzieTerm()

siggersTerm

public static Taylor siggersTerm()

interprets

public Term interprets(Taylor g,
                       int level)

Find a term which in the language of this which satisfies the identities of g.

Parameters:

g -

Returns:

termFromArray

public Term termFromArray(int[] arr)

termFromArray

public Term termFromArray(int[] arr,
                          int start,
                          int len)

makeBalancedTayorTerm

public Term makeBalancedTayorTerm(OperationSymbol f,
                                  int depth,
                                  java.util.List<Variable> varList)

Constructs a term with a balanced term tree. All internal nodes have f and leaves are the variables from varList so varList should have length k^depth, where k is the arity of f.

Parameters:

f -

depth - the depth, at least 1

varList -

Returns:

lexicographicallyCompare

public int lexicographicallyCompare(Term s,
                                    Term t)

lexicographicallyCompare

public static int lexicographicallyCompare(IntArray a,
                                           IntArray b)

lexicographicallyCompare

public static int lexicographicallyCompare(int[] a,
                                           int[] b)

arity

public int arity()

inteqs

public java.util.List<java.util.List<IntArray>> inteqs()

equations

public java.util.List<Equation> equations()

main

public static void main(java.lang.String[] args)