S05

Description

Solutions to Exercises for November 30, 2018

Synopsis

Exercise 4

redexes :: Term -> [Term] Source #

Compute all redexes of a given term.

Exercise 5

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

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