Search code examples
smlmlmosml

Size of propositional-logic formula in Standard ML


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?


Solution

  • 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.