Implementations of various lambda calculus based systems.Source codeContentsIndex
Typed.Term
Stabilityexperimental
Maintainerthanos@sians.org
Contents
Data types
Relations
Subterms and variables
Properties of terms
Supplamentary creators
Substitutions
Description
Terms of the typed system.
Synopsis
data Term
= TmUnit
| TmTrue
| TmFalse
| TmIf Term Term Term
| TmZero
| TmSucc Term
| TmPred Term
| TmIsZero Term
| TmVar String
| TmAbs Typing Term
| TmApp Term Term
| TmWrong String
| TmStop
| TmLoop
type Program = [Term]
(@=) :: Term -> Term -> Bool
subterms :: Term -> [Term]
variables :: Term -> [String]
freeVariables :: Term -> [String]
freeIn :: String -> Term -> Bool
notFreeIn :: String -> Term -> Bool
isUnitVal :: Term -> Bool
isNatVal :: Term -> Bool
isBoolVal :: Term -> Bool
isAbsVal :: Term -> Bool
isVal :: Term -> Bool
natFromInt :: Integral t => t -> Term
abstract :: Term -> Term -> Term
apply :: [Term] -> Term
(|->) :: String -> Term -> Term -> Term
(@>) :: String -> String -> Term -> Term
Data types
data Term Source

Definition of terms for this calculus.

Beware: this, as an instance of Eq, never heard of the alpha-conversion. Use (@=) if you need to check for alpha-equivalence.

Constructors
TmUnitUnit value.
TmTrueBoolean value true.
TmFalseBoolean value false.
TmIf Term Term TermBranching.
TmZeroNatural number zero.
TmSucc TermSuccessor.
TmPred TermPredecessor.
TmIsZero TermZero test.
TmVar StringVariable.
TmAbs Typing TermLambda abstraction.
TmApp Term TermTerm application.
TmWrong StringA term representing an exception-like error.
TmStopStop of evaluation meta-term.
TmLoopA term that loops infinitely.
show/hide Instances
Eq Term
Show Term
type Program = [Term]Source
A list of terms that represent a program.
Relations
(@=) :: Term -> Term -> BoolSource
alpha-conversion equivalence.
Subterms and variables
subterms :: Term -> [Term]Source
List of all subterms of the given term.
variables :: Term -> [String]Source
All variables that occur in the given term.
freeVariables :: Term -> [String]Source
All variables that occur free in the given term.
freeIn :: String -> Term -> BoolSource
Handy shortcut for "x in FV(t)".
notFreeIn :: String -> Term -> BoolSource
"x not in FV(t)". What; this is handy too!
Properties of terms
isUnitVal :: Term -> BoolSource
Checks if the given term is a unit value.
isNatVal :: Term -> BoolSource
Checks if the given term is a natural number value.
isBoolVal :: Term -> BoolSource
Checks if the given term is a boolean value.
isAbsVal :: Term -> BoolSource
Checks if the given term is an abstraction value.
isVal :: Term -> BoolSource
Checks if the given term is a value.
Supplamentary creators
natFromInt :: Integral t => t -> TermSource
Turn an integral number to the corresponding Nat term.
abstract :: Term -> Term -> TermSource
Lambda-abstract a given variable term in a given term.
apply :: [Term] -> TermSource
Turn a list of terms into a single application term. (Like foldr1 TmApp types but returns unit if empty.)
Substitutions
(|->) :: String -> Term -> Term -> TermSource

Substitution in lambda-calculus terms.

(x |-> s) t is the term we get if we replace every free occurrence of x in t with s.

(@>) :: String -> String -> Term -> TermSource

Renaming in the spirit of the alpha-conversion of lambda-calculus.

BEWARE! This isn't safe: w must be correctly picked before-hand. In fact, this is the most brain-dead substitution implementation.

Produced by Haddock version 2.4.2