Simplifying a function OCaml

Learning
1

I m trying to simplify this function as much as possible

let rec f2 a b c d =
match (a,b) with
       |true, false -> a && c || f2 b c a d         (*a is true b is false so it s always true*)
       |true, c -> d && c || f2 b c a d             (*always true*)
       |false, _ -> let d = a || b || c in d        (*only if a==b==c== false else  true*)

My attempt:

 let rec f2 a b c d =
  match (a,b,c) with
   |false, false, false ->   false
   |_,_,_ -> true

I feel that what i tried to do is completely wrong but i dont really know how to correct it, can somebody help me please.

2

perhaps you should look into karnaugh map minimization ?

3

Doesn’t terminate for f2 true true false false and f2 true true true false.

Remember that |true, c -> rebinds c without caring about the previous binding, so the second branch is the same as |true, true -> f2 true true true d.

4

Yes it gives an infinite loop

I dont really get it

5

From where did you get the specification for this function? By which I mean, if the code can give an infinite loop, perhaps better to start with the specification of the function …

6

Try to write it in SMT and run the solver against it.