Lambda UTΒΆ

computation.spad line 856

macro to simplify output

=: (%, %) -> Boolean
return true if equal (deep search) that is: all terms at all levels in tree must be alpha-equivalent to return true That is the names, but not the deBruijn index, of the bound variables can be different. beta-equivalence is not implemented because it is not decidable.
atom?: % -> Boolean
returns true if this is an atom, that is free or bound variable otherwise return false if this is a compound or lambda definition
bind: % -> %
if this is a lambda term then replace string name in sub-nodes with De Bruijn index
coerce: % -> OutputForm
from CoercibleTo OutputForm
free?: % -> Boolean
if this is a lambda term then is it free, that is does its variable appear in its expression
getBoundValue: % -> NonNegativeInteger
introspection: returns deBruijn index of bound variable in bound leaf node
getChildren: % -> List %
returns 2 child nodes if this is a compound term returns 1 child node if this is a lamda term otherwise returns []
getVariable: % -> UT
introspection: returns value of unbound variable in unbound leaf node or bound variable in lambda term
isBoundNode?: % -> Boolean
introspection: returns true if this is a bound leaf node
isCompound?: % -> Boolean
introspection: returns true if this is a compound term containing two nodes
isFreeNode?: % -> Boolean
introspection: returns true if this is a unbound leaf node
isLambda?: % -> Boolean
introspection: returns true if this is a lambda definition
lambda: (%, %) -> %
Constructs a node containing multiple terms
lambda: (%, UT) -> %
Constructs lambda term and bind any variables with the name provided
lambda: NonNegativeInteger -> %
Constructs a reference to a bound variable from its deBruijn index
lambda: UT -> %
Constructs a reference to a free variable
parseLambda: String -> %
Constructs nested lambda terms from a string notation assumes format like this: <term> : :=\" var ”.”<term> | n | <term><term> | “(“<term>”)” where: \ = lambda (I would like to use unicode lambda symbol but I would also like to keep maximum compatibility with non-unicode versions of Lisp) n = De Bruijn index which is a integer where, 1=inside inner lambda term, 2= next outer lambda term, 3= next outer and so on. brackets can be used around whole terms.
parseTerm: (String, NonNegativeInteger) -> Record(rft: %, pout: NonNegativeInteger)
parseTerm is used by parseLambda. It would rarely be called externally but it is here to allow it to call parseLambda that is to allow circular calls
redux: % -> %
beta reduction - apply beta reduction recusivly to all subnodes
subst: (%, %, %) -> %
substitution of ‘a’ for 'b' in 'n'
toString: % -> String
return string representation using deBruijn index for bound variables. notation assumes association to the left, in the absence of brackets, the term to the left binds more tightly than the one on the right.
toStringConven: (%, List String) -> String
return string representation using conventional notation, that is deBruijn index is replaced by name using String value for bound variables. notation assumes association to the left, in the absence of brackets, the term to the left binds more tightly than the one on the right.
unbind: % -> %
if this is a lambda term then replace De Bruijn index in sub-nodes with string name

CoercibleTo OutputForm