at.jku.risc.stout.hoau.algo

Class AntiUnifyProblem

java.lang.Object

at.jku.risc.stout.hoau.algo.AntiUnifyProblem

All Implemented Interfaces:

Equation, Cloneable

public class AntiUnifyProblem
extends Object
implements Equation

This class represents an anti-unification problem (AUP) which consists of one generalization variable (the most general generalization), a list of abstracted bound variables and an anti-unification equation. The list of abstracted variables is additionally stored inside a set for faster lookup.

Author:

Alexander Baumgartner

Field Summary

Fields

Modifier and Type	Field and Description
static String	PRINT_EQ_SEPARATOR
static String	PRINT_VAR_SEPARATOR

Constructor Summary

Constructors

Constructor and Description
AntiUnifyProblem()

Method Summary

Methods

Modifier and Type	Method and Description
boolean	abstrContains(TermAtom boundVar) Tests whether the set of abstracted variables contains the given variable.
BoundVariable	abstrItem(int index) Returns the abstracted bound variable corresponding to the given position index from the list of abstractions.
void	abstrLambda() Abstracts the lambda bound variables of both sides of the equation of this AUP.
Set<BoundVariable>	abstrSet() Returns the set of abstracted variables.
int	abstrSize() Returns the length of the list of abstractions.
void	addAbstrVar(BoundVariable boundVar) Adds a bound variable to the list of abstractions
TermNode	bindAll(TermNode t) Binds all the abstracted variables to the given term.
AntiUnifyProblem	clone()
void	copyAbstr(AntiUnifyProblem eq) Copies the variables from the abstraction list of the given AUP into the abstraction list of this AUP.
TermNode	createHO_Fnc() X(x,y,...) where X is the generalization variable and x,y,...
TermNode	createHO_Fnc(Map<Variable,Variable> pi) X(x,y,...) where X is the generalization variable and x,y,...
TermNode	createLambdaHedge(TermNode lambda) Creates a lambda hedge which contains the given term node and all the abstracted bound variables.
Variable	getGeneralizationVar() Returns the generalization variable, which represents the most general generalization of this AUP.
TermNode	getLeft() Returns the left hand side of the equation.
TermNode	getRight() Returns the right hand side of the equation.
void	setLeft(TermNode left) Sets the left hand side of the equation to the given TermNode.
void	setRight(TermNode right) Sets the right hand side of the equation to the given TermNode.
String	toString()

Methods inherited from class java.lang.Object

equals, getClass, hashCode, notify, notifyAll, wait, wait, wait

Field Detail

PRINT_EQ_SEPARATOR

public static String PRINT_EQ_SEPARATOR

PRINT_VAR_SEPARATOR

public static String PRINT_VAR_SEPARATOR

Constructor Detail

AntiUnifyProblem

public AntiUnifyProblem()

Method Detail

abstrContains

public boolean abstrContains(TermAtom boundVar)

Tests whether the set of abstracted variables contains the given variable.

abstrItem

public BoundVariable abstrItem(int index)

Returns the abstracted bound variable corresponding to the given position index from the list of abstractions.

abstrLambda

public void abstrLambda()

Abstracts the lambda bound variables of both sides of the equation of this AUP. The top atom of both sides has to be a lambda atom!

abstrSet

public Set<BoundVariable> abstrSet()

Returns the set of abstracted variables.

abstrSize

public int abstrSize()

Returns the length of the list of abstractions.

addAbstrVar

public void addAbstrVar(BoundVariable boundVar)

Adds a bound variable to the list of abstractions

bindAll

public TermNode bindAll(TermNode t)

Binds all the abstracted variables to the given term.

clone

public AntiUnifyProblem clone()

Specified by:

clone in interface Equation

Overrides:

clone in class Object

copyAbstr

public void copyAbstr(AntiUnifyProblem eq)

Copies the variables from the abstraction list of the given AUP into the abstraction list of this AUP.

createHO_Fnc

public TermNode createHO_Fnc()

X(x,y,...) where X is the generalization variable and x,y,... are the variables in the abstraction list.

createHO_Fnc

public TermNode createHO_Fnc(Map<Variable,Variable> pi)

X(x,y,...) where X is the generalization variable and x,y,... are the variables in the abstraction list and pi is a variable renaming for x,y,...

createLambdaHedge

public TermNode createLambdaHedge(TermNode lambda)

Creates a lambda hedge which contains the given term node and all the abstracted bound variables. For instance if the list of abstracted variables contains x and y and the given term node consists of only one free variable X, then the created lambda hedge would be (X x y). When substituting X later with a lambda term like \z,v. f[a, z, v] the resulting term will become ((\z,v. f[a, z, v]) x y) and after beta reduction it will be f[a, x, y].

getGeneralizationVar

public Variable getGeneralizationVar()

Returns the generalization variable, which represents the most general generalization of this AUP.

getLeft

public TermNode getLeft()

Description copied from interface: Equation

Returns the left hand side of the equation.

Specified by:

getLeft in interface Equation

getRight

public TermNode getRight()

Description copied from interface: Equation

Returns the right hand side of the equation.

Specified by:

getRight in interface Equation

setLeft

public void setLeft(TermNode left)

Description copied from interface: Equation

Sets the left hand side of the equation to the given TermNode.

Specified by:

setLeft in interface Equation

setRight

public void setRight(TermNode right)

Description copied from interface: Equation

Sets the right hand side of the equation to the given TermNode.

Specified by:

setRight in interface Equation

toString

public String toString()

Overrides:

toString in class Object