EOPL - 2.2.2 - Exercise 2.12

This one asks you to implement alpha, beta and eta conversion on lambda-calculus expressions based on the substitution function of the previous exercise. For this we need a function to see if an identifier occurs free in an expression, similar to the one presented on section 1.3 and easy enough. The conversion functions can then be implemented quite simply:

let rec occurs_free v exp =
   match exp with
     Identifier i when v = i -> true
   | Lambda (x, e) when v <> x -> occurs_free v e
   | App (e1, e2) -> (occurs_free v e1) || (occurs_free v e2)
   | Prim (p, e1, e2) -> (occurs_free v e1) || (occurs_free v e2)
   | _ -> false

let alpha_conversion exp new_id =
   match exp with
     Lambda (id, body) when not (occurs_free new_id body) ->
         Lambda (new_id, lambda_calculus_subst body (Identifier new_id) id)
   | _ -> exp
  
let beta_conversion exp =
   match exp with
     App (Lambda (id, body), e) -> lambda_calculus_subst body e id
   | _ -> exp
  
let eta_conversion exp =
   match exp with
     Lambda (id, App (e, Identifier id'))
     when (id=id') && (not (occurs_free id e)) -> e
   | _ -> exp

These conversion functions simply return the same expression if they aren't of the right form. They could signal an error, depending on the application.

EOPL - 2.2.2 - Exercise 2.11

Exercise 2.11 asks you to correct the definition of a substitution function on the lambda-calculus, to avoid variable capture. To do that, we need function fresh-id from the previous exercise, but alas, we can't use it as is, because it is also asked to extend the definition of a lambda-calculus expression to includes literals and primitives. Nevertheless, it's an easy exercise.

To define the new lambda-calculus expression type, we first define a type to specify primitives:

type Primitive = Sum | Mult

type LPExp = Identifier of string | Lambda of string * LPExp
          | App of LPExp * LPExp | Literal of int
          | Prim of Primitive * LPExp * LPExp

And here is the code for auxiliary functions and the substitution function:

let rec all_ids exp =
   match exp with
     Identifier i -> [i]
   | Lambda (x, e) -> x :: (all_ids e)
   | App (e1, e2) -> (all_ids e1) @ (all_ids e2)
   | _ -> []
  
let fresh_id exp s =
   let syms = all_ids' exp in
   let rec loop n =
       let sym = s + (string_of_int n) in
       if List.mem sym syms then loop (n + 1) else sym in
   loop 0
         
let rec lambda_calculus_subst exp subst_exp subst_id =
   let rec subst exp =
       match exp with
         Identifier id when id = subst_id -> subst_exp
       | Identifier id -> exp
       | Lambda (id, body) when id = subst_id -> exp
       | Lambda (id, body) ->
           let id'=fresh_id body id in
           let body'=lambda_calculus_subst body (Identifier id') id in
           Lambda (id', subst body')
       | App (e1, e2) -> App (subst e1, subst e2)
       | Literal l -> exp
       | Prim (p, e1, e2) -> Prim (p, subst e1, subst e2) in
   subst exp

The substitution function always does an alpha conversion (substitution of the identifier bound by the lambda) unless the bound identifier is the same as the one being substituted for. This surely works, as alpha conversion doesn't change the meaning of a lambda expression. An alternative would be to alpha convert only when a capture would occur, but this would require a further check like

if List.mem id (all_ids body) then
 // do alpha conversion
else
 // just simple substitution

It would make the code bigger, but not better. Both versions require linear scans of the body, so the efficiency shouldn't differ much between them.

EOPL - 2.2.2 - Exercise 2.10

Chapter 2 includes examples and exercises for parsing and unparsing textual representations (e.g. parse-expression on page 51). The parsing functions assume a Scheme reader, and just convert from a list representation to an abstract syntax-tree representation based on define-datatype. The unparsing functions do the converse, from the syntax-tree representation to a list representation. As we don't have a list reader in F#, I skipped the examples and exercises related to parsing and unparsing. I also skipped other exercises that I felt wouldn't add much.

So here is Exercise 2.10 about generating fresh identifiers for renaming of variables that might be captured. I first defined a type for lambda-calculus expressions.

type Exp = Identifier of string | Lambda of string * Exp
        | App of Exp * Exp

Then there's all-ids and a converted version of fresh-id:

let rec all_ids exp =
   match exp with
     Identifier i -> [i]
   | Lambda (x, e) -> x :: (all_ids e)
   | App (e1, e2) -> (all_ids e1) @ (all_ids e2)
  
let fresh_id exp s =
   let syms = all_ids exp in
   let rec loop n =
       let sym = s + (string_of_int n) in
       if List.mem sym syms then loop (n + 1)
       else Identifier sym in
   loop 0

EOPL - Chapter 2, Exercise 2.5

Chapter 2 is about data abstraction. Section 2.1 describes the concepts of interface, representation and implementation, and how a single interface may be implemented by different representations. Not much code there. Section 2.2 presents the constructions define-datatype and cases, to define and pattern-match over variant data types (or disjoint unions, or sum types, choose your preferred terminology). That is roughly equivalent to facilities already present in F#, so there's not much new here.

Exercise 2.5 is a simple pattern-matching exercise to work with the definition of a binary tree data type, expressed in F# as

type BinTree = Leaf of int | Interior of string * BinTree * BinTree

Then we can define max-interior using pattern guards, which aren't available in the Scheme cases construct:

let max_interior bt = 
    let rec maxint t = 
        match t with
          Leaf _ -> failwith "Shouldn't get here"
        | Interior (tag, Leaf l1, Leaf l2) -> (tag, l1 + l2)
        | Interior (tag, Leaf l1, t2) -> 
            let tg, s = maxint t2 in 
            if s > s + l1 then (tg, s) else (tag, s+l1)
        | Interior (tag, t1, Leaf l2) -> 
            let tg, s = maxint t1 in 
            if s > s + l2 then (tg, s) else (tag, s+l2)
        | Interior (tag, t1, t2) -> 
            let tg1, s1 = maxint t1 in
            let tg2, s2 = maxint t2 in
            if s1 > s2 then 
                if s1 > s1 + s2 then (tg1, s1) else (tag, s1+s2)
            else
                if s2 > s1 + s2 then (tg2, s2) else (tag, s1+s2) in
    fst (maxint bt)

But this is a case where it's actually shorter to just use a single pattern match and a conditional, instead of pattern guards:

let max_interior bt = 
    let rec maxint t = 
        match t with
          Leaf i -> (None, i)
        | Interior (tag, t1, t2) -> 
            let tg1, s1 = maxint t1 in
            let tg2, s2 = maxint t2 in
            if tg1 = None && tg2 = None then
                (Some tag, s1 + s2)
            elif s1 > s2 || tg2 = None then
                if s1 > s1+s2 then (tg1, s1) 
                else (Some tag, s1+s2)
            else
                if s2 > s1+s2 then (tg2, s2) 
                else (Some tag, s1+s2) in
    match bt with
      Leaf _ -> failwith "Shouldn't happen"
    | t -> maxint t |> fst |> Option.get

Even so, the function is somewhat big, and could be broken in two, but we'll let it as it is.

Scala

My choice for a functional programming language that integrates with .NET is F#. By the same token, when I think about writing software for the Java platform and wish to use a language better suited to my tastes, my choice is Scala. It's a pretty cool language that mixes OO and functional programming quite neatly, and with interesting theoretical studies to support it. The syntax was chosen to be similar to Java, which I don't like, but it's a minor problem. It's actively supported and developed, and is gaining momentum right now, which can be a good thing.

I need to write a simple program to talk to a Java program in the next few days, so I'll probably be using Scala for it. This means I may write posts about it in the near future.