Safe HaskellSafe

Term

Contents

Synopsis

Exercises 2 and 3

See ../pdfs/05.pdf.

type Id = String Source #

Identifiers as Strings.

data Term Source #

Lambda terms: variables, application, abstraction.

Constructors

Var Id 
App Term Term 
Abs Id Term 

Instances

Show Term #

Custom Show instance for readability.

Methods

showsPrec :: Int -> Term -> ShowS

show :: Term -> String

showList :: [Term] -> ShowS

Exercise 4

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"]

Exercise 5

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'.

Exercise 6

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"))