Size of propositional-logic formula in Standard ML

Question

I'm working on this problem, where the propositional logic formula is represented by:

datatype fmla =
     F_Var of string
   | F_Not of fmla
   | F_And of fmla * fmla
   | F_Or of fmla * fmla 

Im trying to write a function that returns the size of a propositional-logic formula. A propositional variable has size 1; logical negation has size 1 plus the size of its sub-formula; logical conjunction and disjunction have size 1 plus the sizes of their sub-formulas.

How would I go about trying to solve this problem?

Answer 1

In general, when you have a sum type like this, it can be a good idea to start with a function definition that just lists each case but leaves out the implementation:

fun size (F_Var v) =
  | size (F_Not f) =        
  | size (F_And (f1, f2)) =
  | size (F_Or (f1, f2)) =

and then you fill in the definitions of the cases one at a time as you figure them out.

Since you already have a list of what the size is in each case;

• A propositional variable has size 1.
• A negation has size 1 plus the size of its sub-formula.
• A conjunction has size 1 plus the sum of the sizes of its sub-formulas.
• A disjunction has size 1 plus the sum of the sizes of its sub-formulas.

you can pretty much translate it directly into ML:

fun size (F_Var _) = 1
  | size (F_Not f) = 1 + size f
  | size (F_And (f1, f2)) = ...
  | size (F_Or (f1, f2)) = ...

where I have left two cases for you to fill in.
Note that there is a very close correspondence between the definition in English and the definition in ML of each case.