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.