SKICombinators(UT)

computation.spad line 1631 [edit on github]

• UT : VarCat

This domain implements SKI combinators. Ski combinators were introduced by Moses Schoenfinkel and Haskell Curry with the aim of eliminating the need for variables in mathematical logic. It is equivalent to lambda calculus but it can be used for doing, without variables, anything that would require variables in other systems.

= : (%, %) -> Boolean

return true if equal (deep search) that is: all terms at all levels in tree must be equal to return true all terms must be exactly equal, not just equivalent, that is SKK=I will return false even though 'SKK' and 'I' have the same effect

I : () -> %

Constructs a I combinator

K : () -> %

Constructs a K combinator

S : () -> %

Constructs a S combinator

atom? : % -> Boolean

returns true if this is an atom, that is a leaf node otherwise return false if this is a compound term

coerce : % -> OutputForm

from CoercibleTo(OutputForm)

freeVariable? : (%, UT) -> Boolean

the variable indicated by 's' is free if it does not appear in node 'n' or any of its subnodes.

getChildren : % -> List(%)

returns child nodes if this is a compound term otherwise returns []

getVariable : % -> UT

returns the variable, if this is not a variable then return I

isI? : % -> Boolean

returns true if this is an I combinator node

isK? : % -> Boolean

returns true if this is a K combinator node

isS? : % -> Boolean

returns true if this is a S combinator node

latex : % -> String

from SetCategory

parseSki : String -> %

Constructs combinators from a string

parseTerm : (String, NonNegativeInteger) -> Record(rft : %, pout : NonNegativeInteger)

parseTerm is used by parseSki. It would rarely be called externally but it is here to allow it to call parseSki that is to allow circular calls

redux : % -> %

weak reduction - apply this combinator to rearrange its subnodes then apply recursively to its subnodes.

ski : (%, %) -> %

Constructs a node combinator over combinators

ski : UT -> %

Constructs variable combinator

toString : % -> String

output

variable? : % -> Boolean

returns true if this is an variable

~= : (%, %) -> Boolean

from BasicType

CoercibleTo(OutputForm)

BasicType

SetCategory