Homework 1

Due: Sunday, September 14th at 11:59pm

Setting up OCaml

First, if you haven't already, set up OCaml. Instructions can be found here.

Submission Instructions

Start with the template code here.

• Replace each failwith "TODO" with your solution. (failwith has type string -> t for any type t, and throws an exception when it evaluates. Your solution to each problem should not include failwith.)
• Be sure to test your solutions in utop or in tests alongside your submission. To load your file into utop, use #use "hw1.ml":

  > utop # #use "hw1.ml";;
  val implies : bool -> bool -> bool = <fun>
  val implies_if : bool -> bool -> bool = <fun>
  val p1 : bool -> bool -> bool -> bool -> bool = <fun>
  val p2 : bool -> bool -> bool -> bool = <fun>
  val p3 : bool -> bool -> bool -> bool = <fun>
  val p4 : bool -> bool -> bool = <fun>
  val forallb : (bool -> bool) -> bool = <fun>
  val existsb : (bool -> bool) -> bool = <fun>
  val lemma_1 : unit -> bool = <fun>
  val lemma_2 : unit -> bool = <fun>
  val lemma_3 : unit -> bool = <fun>
  val prop_complex : bool -> bool -> bool = <fun>
  val prop_simple : bool -> bool -> bool = <fun>
  val prop_simple_lemma : unit -> bool = <fun>
  val forall_0_5 : (int -> bool) -> bool = <fun>
  val exists_0_5 : (int -> bool) -> bool = <fun>
  val lemma_4 : unit -> bool = <fun>
  val lemma_5 : unit -> bool = <fun>
  

  You can then call each function to inspect its behavior.
• Submit your version of hw1.ml to the HW1 assignment on Gradescope. Your version of hw1.ml should include (at least) the functions above, with the same types as above.

Propositional Logic

In Discrete, you learned about propositional logic: a mathematical way to reason about truth. We can encode ideas from propositional logic into OCaml by modeling propositions (e.g., \(P\), \(Q\), \(P \wedge Q\)) as expressions of type bool. OCaml. Below is a table of common logical operators, along with their OCaml counterparts. On the OCaml side, p and q are variables of type bool.

Propsitional Logic	OCaml
True	true
False	false
\(P \wedge Q\)	p && q
\(P \vee Q\)	p || q
\(\neg P\)	not p

Q1: Implication

An important operation in propositional logic is implication, written \(P \implies Q\). \(P \implies Q\) is true if, whenever \(P\) is true, \(Q\) must be true as well (or equivalently, whenever \(Q\) is false, \(P\) must be false). Below is the truth table for \(P \implies Q\):

\(P\)	\(Q\)	\(P \implies Q\)
true	true	true
true	false	false
false	true	true
false	false	true

While logical implication is important for propositional logic, it is typically not built into programming languages. Nevertheless, we can encode it in OCaml. For Q1, implement implies : bool -> bool -> bool by using &&, || and not:

let implies (p : bool) (q : bool) : bool = 
    failwith "TODO" (* Replace with your implementation here. *)

Then, implement implies_if : bool -> bool -> bool by instead ONLY using if/then/else expressions (as well as the boolean constants true and false, if you need them). Do NOT use &&, ||, or not.

let implies_if (p : bool) (q : bool) : bool = 
    failwith "TODO" 

Note: let-defined functions and multi-argument functions

Defining a function as follows:

let implies (p : bool) (q : bool) : bool = ...

is the same as:

let implies = fun (p : bool) (q : bool) -> ...

and thus, implies has type bool -> (bool -> bool). Type arrows are right associative, so this is usually written as bool -> bool -> bool.

We can also write implies as

let implies = fun (p : bool) -> fun (q : bool) -> ...

since multi-argument functions are equivalently functions on earlier arguments to functions on later arguments.

Note: calling multi-argument functions

Because implies has type bool -> bool -> bool, you can either call it in full, or call it on the first argument to get another function of type bool -> bool.

utop# let implies (p : bool) (q : bool) : bool = true;; (* NOT the correct solution, just a placeholder so we don't see the exception *)
val implies : bool -> bool -> bool = <fun>

utop# implies false true;; (* Calling on both arguments *)
- : bool = true

utop# let f = implies false;; (* Partially applying `implies` on one argument *)
val f : bool -> bool = <fun>

utop# f true;;
- : bool = true

This works because application of two arguments, such as implies false true, is parsed like (implies false) true. Thus, implies false true is the same as let f = implies false in f true.

Q2: Translating propositional logic

Now, translate the following logical formulas into OCaml boolean expressions. You may only use the basic Boolean operators &&, ||, not, and your implementation of implies from Q1.

• \((P \wedge Q) \vee (\neg (R \wedge S))\)
  • NOTE: A previous version of this document listed \((P \wedge Q) \vee (\neg (R \vee S))\), while hw1.ml has \((P \wedge Q) \vee (\neg (R \wedge S))\) (notice the last subterm). The version listed here with \(R \vee S\) was a typo; we will accept either version.
• \((P \vee Q) \Rightarrow (\neg R)\)
• \(\neg (P \wedge (Q \vee R))\)
• \((P \Rightarrow Q) \wedge (Q \Rightarrow P)\)

Q3: Forall and Exists on Booleans

In addition to the basic logical connectives (\(\wedge\), \(\vee\), \(\neg\), \(\implies\)), we can also encode quantification (\(\forall\) and \(\exists\)) in OCaml in certain cases, depending on the sets we are quantifying over. Quantifying over infinite types (such as the natural numbers) is hard to encode into booleans, but quantifying over finite types is easier.

In this question, you will implement universal and existential quantification over booleans; i.e., \(\forall x \in \mathsf{bool}, P(x)\) and \(\exists x \in \mathsf{bool}, Q(x)\). Because \(P\) and \(Q\) expect a value of type bool, \(P\) and \(Q\) will be functions. And thus, your implementations of \(\forall\) and \(\exists\) will be higher-order functions: functions which take a function as input.

let forallb (f : bool -> bool) : bool = failwith "TODO"

let existsb (f : bool -> bool) : bool = failwith "TODO"

Hint

Can you write \(\forall x \in \mathsf{bool}, P(x)\) as an equivalent proposition that doesn't use quantification?

Q4: Verifying Equivalences

Now let's validate your implementations in Q3. Using forallb and existsb, implement the following propositions:

• lemma_1: \(\forall p \in \mathsf{bool}, (p \wedge p) = p\)
• lemma_2: \(\forall p \in \mathsf{bool}, \exists q \in \mathsf{bool}, (p \wedge q) = p\)
• lemma_3: \(\forall p \in \mathsf{bool}, \forall q \in \mathsf{bool}, (\neg p \implies q) = (p \vee q)\).

Each proposition will be implemented as a function from unit -> bool. We do this by writing () as one of the arguments (which matches the unique of type unit.) For example:

let lemma_1 () : bool = failwith "TODO"

While each lemma has type bool, it should not be simply defined to be true or false; your solutions should use forallb and existsb from the previous problem to compute the truth values of the above propositions.

Hint

To translate lemma_1 into OCaml, you will need to pass a function as an argument to forallb.

Q5: Simplifying Propositions

Here, we have given you the proposition \(\neg P \vee Q \vee P\):

let prop_complex (p : bool) (q : bool) : bool = 
    (not p) || q || p

There exists an equivalent, but much simpler, proposition. (Here, "equivalent" means "has the same truth table".) Implement it in prop_simple. Then, use forallb which you implemented in Q3 to verify that prop_simple is equivalent to prop_complex:

(* forall q : bool, forall q : bool,  prop_complex p q = prop_simple p q *)
let prop_simple_lemma : bool = failwith "TODO"

Q6: Forall, Exists on [0..5]

Here, we will build upon the forallb and existsb functions you designed in Q3 to create versions which operate over the integers from 0 to 5 (inclusive, meaning the set of integers \(\{0, 1, 2, 3, 4, 5\}\)):

• forall_0_5, corresponding to \(\forall\) over the integers [0,5], and
• exists_0_5, corresponding to \(\exists\) over the integers [0,5].

The functions forall_0_5 and exists_0_5 both expect an argument of type int -> bool, which we interpret as a predicate P(x) where x is an integer. While P(x) might be defined for more integers than just those between 0 and 5, your solution won't need to worry about the behavior of P outside of [0,5].

Q7: Formalizing properties on integers

Similar to Q4, we can validate the implementations in Q6 by using them to compute the truth value of various propositions:

• lemma_4: \(\forall x \in [0..5], \exists y \in [0..5], x - y = 0\)
• lemma_5: \(\forall x \in [0..5], (x\ \mathsf{mod}\ 2) = 0 \Rightarrow (\exists k \in [0..5], x = 2 * k)\)

Here we'll need to use OCaml's basic operations on the integers: +, *, -, and mod. Your solutions will be similar to those in Q4, but using forall_0_5/exists_0_5.