Lambda(UT)

computation.spad line 856 [edit on github]

• UT : VarCat

An implementation of untyped lambda-calculus

= : (%, %) -> 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 lambda 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 : UT -> %

Constructs a reference to a free variable

lambda : NonNegativeInteger -> %

Constructs a reference to a bound variable from its deBruijn index

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)