Safe HaskellSafe



A Module for Lambda-Terms.



type Id = String Source #

Identifiers as Strings.

data Term Source #

Lambda terms: variables, application, abstraction.


Var Id 
App Term Term 
Abs Id Term 


Show Term #

Custom Show instance for readability.


showsPrec :: Int -> Term -> ShowS #

show :: Term -> String #

showList :: [Term] -> ShowS #

redexes :: Term -> [Term] Source #

Compute all redexes of a given term.

vars :: Term -> [Id] Source #

The set of all variables occurring in a term. For example

vars (App (Var "x") (Abs "y" (Var "y"))) == ["x", "y"]

fvs :: Term -> [Id] Source #

The set of free variables occurring in a term. For example

fvs (App (Var "x") (Abs "y" (Var "y"))) == ["x"]

freshName :: Id -> [Id] -> (Id, Term -> Term) Source #

Given a variable x and a set of variable names to avoid ys, freshName x ys computes a pair (x', ren) such that x' is a variable that is fresh for ys (that is, different from all elements of ys) and ren :: Term -> Term is a function that renames all occurrences of x in a term by x'.

subst :: Id -> Term -> Term -> Term Source #

Applying a substition [x := s] to a lambda term t. For example (note how the bound variable "y" is renamed in order to avoid variable capture)

subst "x" (Var "y") (Abs "y" (App (Var "x") (Var "y"))) == Abs "z" (App (Var "y") (Var "z"))

showsPrecTerm :: Int -> Term -> ShowS Source #

showsPrecTerm n t transforms term t within a context of precedence n into a "string" (for efficiency reasons actually the type ShowS is used).