Functional Programming & Proofs


Trees and languages

  1. (recursive datayes, trees, abstract syntax)
    How to define set of boolean expressions ?
  2. How to print or evaluate boolean expressions ?
type BExp = BVal of Bool | BNot of BExp | BAnd of BExp*BExp;;

let rec beval be = 
  match be with
  | BVal v         -> v
  | BNot be1       -> Not (beval be1)
  | BAnd (be1,be2) -> And (beval be1) (beval be2);;

let be = BAnd (BVal True,BNot (BVal False));;
beval be;;

let rec bstring be = 
  match be with
  | BVal True       -> "True"
  | BVal False      -> "False"
  | BNot be1       -> "(Not "+(bstring be1)+")"
  | BAnd (be1,be2) -> (bstring be1)+" <&> "+(bstring be2);;

(bstring be)," = ", (beval be);;
printfn "%s = %A" (bstring be) (beval be);;

4 - 10