# Lambda UT¶

computation.spad line 856 [edit on github]

UT: VarCat

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