From complete unit tests to implementation

Mimer: Observational equivalence at work.

Loki: Right. Not iffy at all.

The goal of this lecture note is to illustrate how to calculate implementations from complete specifications. The calculations are spelled out for Boolean functions (negation, conjunction, etc.). The resulting definitions only use conditional expressions.

These resulting definitions are discovered, not invented, and since their starting point and their calculation are correct, they are correct by construction.

Resources

• The OCaml code for the present lecture note (latest version: 18 Sep 2022).

The observational equivalences

• for any expression e, if e then true else false and e are observationally equivalent
• for any pure expression v, if v then true else true and true are observationally equivalent
• for any pure expression v, if v then false else false and false are observationally equivalent

Negation

Let us revisit Exercise 15 from Week 03. The following unit-test function is complete in that it enumerates the graph of the negation function:

let test_not candidate =
  let b0 = (candidate true  = false)
  and b1 = (candidate false = true)
  in b0 && b1;;

OCaml’s predefined negation function passes this unit test.

Our witness implementation mimicks this unit-test function the way a fake function would:

let witness_not b =
  if b = true
  then false
  else (if b = false
        then true
        else undefined ());;

where undefined is summarily defined as a failed assertion:

let undefined () =
  assert false;;

This witness implementation passes the unit test.

Our starting point distinguishes between the two possible arguments for negation, and uses witness_not to return the right result:

let not_v1 b =
  if b
  then witness_not true
  else witness_not false;;

This implementation passes the unit test.

We then unfold the calls to witness_not and select the corresponding conditional branch:

let not_v2 b =
  if b
  then false
  else true;;

This implementation passes the unit test, is self-contained, and only uses conditional expressions.

Conjunction

Let us revisit Exercise 02 from Week 04. The following unit-test function is complete in that it enumerates the graph of the conjunction function:

let test_and candidate =
  let b0 = (candidate true  true  = true)
  and b1 = (candidate true  false = false)
  and b2 = (candidate false true  = false)
  and b3 = (candidate false false = false)
  in b0 && b1 && b2 && b3;;

OCaml’s predefined conjunction function passes this unit test.

Our witness implementation mimicks the unit-test function the way a fake function would:

let witness_and b1 b2 =
  if b1 = true && b2 = true
  then true
  else (if b1 = true && b2 = false
        then false
        else (if b1 = false && b2 = true
              then false
              else (if b1 = false && b2 = false
                    then false
                    else undefined ())));;

Our starting point distinguishes between the four possible arguments for conjunction, and uses witness_and to return the right result:

let and_v1 b1 b2 =
  if b1
  then (if b2
        then witness_and true true
        else witness_and true false)
  else (if b2
        then witness_and false true
        else witness_and false false);;

This implementation passes the unit test.

We then unfold the calls to witness_and and select the corresponding conditional branch:

let and_v2 b1 b2 =
  if b1
  then (if b2
        then true
        else false)
  else (if b2
        then false
        else false);;

On the ground that

• if b2 then true else false and b2 are observationally equivalent, and
• if b2 then false else false and false are observationally equivalent too,

we simplify and_v2 into the final implementation:

let and_v3 b1 b2 =
  if b1
  then b2
  else false;;

This implementation passes the unit test, is self-contained, and only uses conditional expressions.

Exercise 16 – disjunction

Revisiting Exercise 03 from Week 04, calculate an implementation of boolean disjunction, based on the following unit-test function, which is complete:

let test_or candidate =
  let b0 = (candidate true true = true)
  and b1 = (candidate true false = true)
  and b2 = (candidate false true = true)
  and b3 = (candidate false false = false)
  in b0 && b1 && b2 && b3;;

Exercise 17 – negated conjunction (nand)

Revisiting Exercise 04 from Week 04, calculate an implementation of negated conjunction (a.k.a. the Sheffer stroke), based on the following unit-test function, which is complete:

let test_nand candidate =
  let b0 = (candidate true  true  = false)
  and b1 = (candidate true  false = true)
  and b2 = (candidate false true  = true)
  and b3 = (candidate false false = true)
  in b0 && b1 && b2 && b3;;

Exercise 18 – negated disjunction (nor)

Revisiting Exercise 05 from Week 04, calculate an implementation of negated disjunction (a.k.a. Peirce’s arrow), based on the following unit-test function, which is complete:

let test_nor candidate =
  let b0 = (candidate true  true  = false)
  and b1 = (candidate true  false = false)
  and b2 = (candidate false true  = false)
  and b3 = (candidate false false = true)
  in b0 && b1 && b2 && b3;;

Exercise 19 – exclusive disjunction (xor)

Revisiting Exercise 06 from Week 04, calculate an implementation of exclusive disjunction based on the following unit-test function, which is complete:

let test_xor candidate =
  let b0 = (candidate true  true  = false)
  and b1 = (candidate true  false = true)
  and b2 = (candidate false true  = true)
  and b3 = (candidate false false = false)
  in b0 && b1 && b2 && b3;;

Exercise 20 – implication

Calculate an implementation of boolean implication based on the following unit-test function, which is complete:

let test_implies candidate =
  let b0 = (candidate true  true  = true)   (* true implies true *)
  and b1 = (candidate true  false = false)  (* true does not imply false *)
  and b2 = (candidate false true  = true)   (* false implies anything *)
  and b3 = (candidate false false = true)   (* false implies anything *)
  in b0 && b1 && b2 && b3;;

Exercise 21 – equivalence

Calculate an implementation of boolean equivalence based on the following unit-test function, which is complete:

let test_equivalence candidate =
  let b0 = (candidate true   true = true)   (* true and true are equivalent *)
  and b1 = (candidate true  false = false)  (* true and false are not equivalent *)
  and b2 = (candidate false  true = false)  (* false and true are not equivalent *)
  and b3 = (candidate false false = true)   (* false and false are equivalent *)
  in b0 && b1 && b2 && b3;;

Exercise 22

Confirm (in two distinct ways) or deny (with one counter-example) the following rumoured observational equivalences:

1. For any boolean value b, are b && b and b observationally equivalent?
2. For any boolean value b, are b || b and b observationally equivalent?
3. For any boolean values b1 and b2, are not (b1 && b2) and (not b1) || (not b2) observationally equivalent?
4. For any boolean value b1 and b2, are not (b1 || b2) and (not b1) && (not b2) observationally equivalent?

Exercise 23

Confirm (in two distinct ways) or deny (with one counter-example) the following rumoured observational equivalences:

1. For any boolean value b, are not b and nand b b observationally equivalent?
2. For any boolean values b1 and b2, are b1 && b2 and nand (nand b1 b2) (nand b1 b2) observationally equivalent?
3. For any boolean values b1 and b2, are b1 || b2 and nand (nand b1 b1) (nand b2 b2) observationally equivalent?

Exercise 24

Confirm (in two distinct ways) or deny (with one counter-example) the following rumoured observational equivalences:

1. For any boolean value b, are not b and nor b b observationally equivalent?
2. For any boolean values b1 and b2, are b1 && b2 and nor (nor b1 b2) (nor b1 b2) observationally equivalent?
3. For any boolean values b1 and b2, are b1 || b2 and nor (nor b1 b1) (nor b2 b2) observationally equivalent?

Exercise 25

Confirm (in two distinct ways) or deny (with one counter-example) the following rumoured observational equivalences:

1. For any boolean values b1 and b2, are implies b1 b2 and not b1 || b2 observationally equivalent?
2. For any boolean values b1 and b2, are not (implies b1 b2) and b1 || not b2 observationally equivalent?
3. For any boolean values b1 and b2, are implies b1 b2 && implies b2 b1 and equivalent b1 b2 observationally equivalent?
4. For any boolean values b1, b2, and b3, are implies b1 (implies b2 b3) and implies (b1 && b2) b3 observationally equivalent?
5. For any boolean values b1, b2, and b3, are (implies b1 b3) && (implies b2 b3) and implies (b1 || b2) b3 observationally equivalent?
6. For any boolean values b1, b2, and b3, are (implies b1 b3) || (implies b2 b3) and implies (b1 && b2) b3 observationally equivalent?

Resources

• The OCaml code for the present lecture note (latest version: 18 Sep 2022).

Version

Created [10 Jan 2023]