proof.term
Interface Term

All Superinterfaces:

java.io.Serializable

All Known Implementing Classes:

Abstr, Appl, EmptyRecord, EmptyRecordType, Field, Pair, Pi, Sigma, Sort, Var

public interface Term

extends java.io.Serializable

An attempt at implementing terms using references to handle variable binding.

Method Summary

boolean	alphaEquals(Term t) Compares this term to another term, up to variable renaming.
Term	headReduceOnce() Reduces this term once in lazy order.
Term	substitute(Var y, Term t) Calculates the result of substituting into this term.
java.lang.String	toString() Convert this term to a string.

Method Detail

substitute

public Term substitute(Var y,
                       Term t)

Calculates the result of substituting into this term. If possible, it returns a copy, but it shouldn't destructively modify anything.

Parameters:

y - the Var to substitute in for

t - the term to substitute in.

Returns:

the result of substituting

headReduceOnce

public Term headReduceOnce()

Reduces this term once in lazy order. This actually reduces more than that usually, so perhaps it should be renamed.

Returns:

this term, reduced once

alphaEquals

public boolean alphaEquals(Term t)

Compares this term to another term, up to variable renaming.

Parameters:

t - the term to compare this to

Returns:

true iff this and t are equal (ignoring the names of variables)

toString

public java.lang.String toString()

Convert this term to a string. There's no guarantee that the resulting term will be parseable.

Overrides:

toString in class java.lang.Object