Wednesday, March 7, 2007

EOPL - 2.3.4 - Exercise 2.24

This exercise asks for an implementation of substitutions on terms, the terms being defined by a previous exercise (2.13). In F#, they are thus defined:

type Value = Integer of int | String of string
type Term = Id of string | Constant of Value | App of Term list

let rec term_all_ids t =
match t with
Id s -> [s]
| Constant _ -> []
| App tl -> List.concat (List.map term_all_ids tl)

Function term_all_ids gets all identifiers from a term, also part of exercise 2.13. Then for the part specific to exercise 2.24, which are substitutions. I chose to use an abstract syntax tree representation, because it is more convenient in F#. Using the definition, it was easy to write the operations on substitutions.

type Subst = EmptySub | ExtendedSub of string * Term * Subst

let empty_subst () =
EmptySub

let extend_subst i t s =
ExtendedSub (i, t, s)

let rec apply_subst s i =
match s with
EmptySub -> Id i
| ExtendedSub (i', t, s') when i = i' -> t
| ExtendedSub (_, _, s') -> apply_subst s' i

With the substitution data type completed, we can write a substitution function without any difficulties.

let rec subst_in_term s t =
match t with
Id i -> apply_subst s i
| Constant _ -> t
| App tl -> App (List.map (subst_in_term s) tl)

let subst_in_terms lt s =
List.map (subst_in_term s) lt

I guess subst_in_terms might have been intended as a little more difficult to write. I don't know. In any case, it's just a map.

No comments: