Logical contradiction type definitions

Question

(Homework alert)

Working my way through "The Haskell Road...", not sure about my solution to exercise 2.15 on page 48 of the second edition:

A propositional contradiction is a formula that yields false for every combination of truth values for its propositional letters. Write Haskell definitions of contradiction tests for propositional functions with one, two, and three variables.

I somehow gather from the way the question is asked that they expect something along the lines of:

contradiction_1 :: (Bool -> Bool) -> Bool
contradiction_1 f = (f True) == False && (f False) == False

and so on.

However, previously in the text it has been shown how to use a type class to implement validity and logical equivalence:

{-# LANGUAGE FlexibleInstances #-}
class TF p where
 valid :: p -> Bool
 lequiv :: p -> p -> Bool
instance TF Bool where
 valid = id
 lequiv f g = f == g
instance TF p => (Bool -> p) where
 valid = valid (f True)
 && valid (f False)
 lequiv f g = lequiv (f True) (g True)
 && lequiv (f False) (g False)

This above is all in the textbook.

So I thought that I can simply add the definition for contradiction as follows:

class TF p where
 valid :: p -> Bool
 contradiction :: p -> Bool -- added
 lequiv :: p -> p -> Bool
instance TF Bool where
 valid = id
 contradiction f = f == False -- added
 lequiv f g = f == g
instance TF p => (Bool -> p) where
 valid = valid (f True)
 && valid (f False)
 contradiction f = contradiction (f True) -- added
 && contradiction (f False) -- added
 lequiv f g = lequiv (f True) (g True)
 && lequiv (f False) (g False)

This now is the code from the textbook, still unchanged, only with my additions.

It seems to work, in the sense that it only returns true for actual contradictions for what I've tried so far, for example, with GHCI:

*Main> contradiction (\p -> p && (not p))
True
*Main> contradiction (\p q -> (p || q) && ((not p) && (not q)))
True
*Main> contradiction (\p q r -> p && q && ((not p) && r))
True

But I have to admit that I really don't understand what exactly the code I wrote is doing (I did it with "pattern matching", if you know what I mean).

PS: I cannot tag the question as I would like because I don't have enough rep to create new tags.

• Myridium: This interests me, as I've been looking into both Haskell and theorem provers... I can't help much though, sorry. Two things I will suggest: 1. It looks nice when you align things i.e. insert whitespace so that the :: symbols line up. 2. Instead of contradiction f = f == false, why not contradiction = not.id? This makes it the logical negation of id.
• XXX: @Myridium I haven't written much Haskell code and I am still finding the most comfortable spacing/indenting style. The second suggestion though... "Contradiction" is meant to mean "formula is false for any combination of variable values", so I think the logical negation of id would be actually wrong?
• Myridium: contradiction f = (f == False) is applied to an instance of the typeclass TF a where a => Bool (a is of type Bool). This means that in that expression you have, f is simply a Bool-- it is either True or False. So in this case, I think all you want to do is take the negation of f.
• XXX: @Myridium Why don't you write an answer?
• Myridium: I have never even written my own typeclass before; I'm hardly qualified to write an answer. However, if you want to enter a chat room and work together on understanding this, then I would be happy to do so.

Answer 1

Alright, this is the first time I've used Typeclasses so someone feel free to slap me with a tuna if I mess something up.

First of all, I don't understand why the use of "FlexibleInstances" is necessary, and it scares me because these kinds of warnings are usually put in place for a reason. With that out of the way, I'll go through the code.

---

The first thing you should realize is that in Haskell, typeclasses are basically the same thing as Java's interfaces. They define a contract of behaviour which instances of the class must obey. In this case, the typeclass I'm calling Prop promises the user three methods:

1. valid to check if the proposition is logically valid (true for all possible inputs)
2. contradiction to check if the proposition is false for all possible inputs.
3. lequiv to check if two propositions of the same number of arguments have an identical truth value given the same inputs.

These correspond to three questions which we could ask of any proposition which is a function of any number of propositional atoms. In case you're unfamiliar with this terminology, an 'atom' is one of the inputs to a proposition which is a function taking some number of atoms and itself evaluating to either True or False.

Typeclass Declaration

The name TF for the type class bears no meaning for me, so I changed it to Prop short for "Proposition".

-- A typeclass which different types may implement.
class Prop p where
 valid :: p -> Bool -- Same thing as a Tautism
 contradiction :: p -> Bool -- False under all conditions/opposite of Tautism
 lequiv :: p -> p -> Bool 

What we're doing here is creating a new typeclass called Prop. We need the syntax Prop p because we need to define the behaviour of an instance p of the Prop class. If we don't introduce a symbol for it, then how will the compiler know what we're talking about the in the typeclass definition? For example, the line valid :: p -> Bool says that for every instance p of typeclass Prop, there must be a method called valid which maps p to a boolean value. Likewise, there must be a similar method for contradiction.

Now the line lequiv :: p -> p -> Bool may cause some confusion because p appears twice. It's important to understand that p, being an instance of a typeclass, is a type. There are no "objects" as in object-oriented languages. Remember: p is a type which satisfies the typeclass contract given by Prop. The Java equivalent would be a class p implementing an interface Prop. What we're saying here is that for type which implements/is a part of this typeclass Prop, there is a method called lequiv of comparing them. And its type is p -> p -> Bool meaning that it takes in two expressions of type p and returns a boolean indicating whether or not they're equivalent.

---

Boolean Instance Definition

All we've told the compiler so far are our promises: there will be methods for checking whether an instance of Prop is valid or a contradiction, and a method for comparing two propositions of the same type for equality.

To start, we implement these procedures for the most basic type of proposition: one that is just True or False.

-- This is a proposition which is simply a literal Bool!
instance Prop Bool where
 valid = id
 contradiction = not
 lequiv b1 b2 = b1 == b2

Here, Prop Bool says that in the expression Prop p above, the type whose behaviour/implementation we're defining is the Bool type. How do we check if a Bool is valid? Well, it takes no arguments, so a proposition that is just True or False is valid if it's true, and otherwise a contradiction.

1. valid = id says that the function valid mapping our proposition type of Bool to whether or not it's a valid formula is the function id. (This function just returns whatever it's given).
2. contradiction = not says that the function contradiction mapping the proposition type Bool to whether or not it's a contradiction is the function not. Just as well, because not takes just one Bool as an argument, and returns a Bool. This is compatible with the contract we laid out earlier in the typeclass definition of Prop.
3. lequiv b1 b2 = (b1 == b2) says that the way of comparing two of these propositions (once again, of type Bool here) for logical equivalence is to simply invoke the already existing method ==.

---

Inductive Instance Definition - First Step

This is the fun part. We're using induction. Here's the full code snippet, and then I'll break down each line.

instance (Prop p) => Prop (Bool -> p) where
 valid f = (valid (f True)) && (valid (f False))
 lequiv f g = (lequiv (f True) (g True)) && (lequiv (f False) (g False))
 contradiction f = (contradiction $ f True) && (contradiction $ f False)

Now the first line says this: (Bool -> p) is of type Prop, as long as the constraints in what we call the context are met. Here the context is what comes before the =>, and what it says is that p, the type, is a member of the Prop typeclass. This means that we're saying that any type which maps a Bool to any type of Prop is itself an instance of Prop. Why are we doing this? Well, let's start with the simplest case.

Bool is an instance of typeclass Prop, because we defined this 'base case' explicitly. Okay, so then (Bool -> Bool) is also of typeclass prop, because we said that any type (Bool -> <something in class Prop>) is in class Prop. This gives us the functions which take in one boolean argument and return a boolean. Examples: not, id, (\a -> True), (\a -> False). (In fact, these are all such functions).

How have we defined whether to determine whether one of these functions is valid? Our definition says that

valid f = (valid (f True)) && (valid (f False))

It says that a boolean function f of one boolean is valid if and only if (f True) and (f False) are both valid. Of course, the validity of boolean is just that boolean. So in this case, valid can be thought of as being a bit simpler:

valid f = (f True) && (f False)

Alright, so f is valid if and only if it evaluates to True for both arguments! That's what we want.

Now for contradiction:

contradiction f = (contradiction $ f True) && (contradiction $ f False)

This is the key: contradiction asks the question "Is this proposition false for all possible inputs"? To test this, we split f into two parts: its first argument and the rest. If the first argument is True, then is it possible to satisfy proposition f with the remaining arguments? If not, then it's a contradiction. This is the part contradiction $ f True.

f True is itself a function of 1 Bool argument, so it is in class Prop, and so we're able to apply contradiction to it to see if it's a contradiction. We also need to be sure that it's not possible to satisfy f if the first argument is False either, which is why we && this with contradiction $ f False.

I'll leave the lequiv function as an exercise, and move on to the next inductive step.

Inductive Instance Definition - Inception

Since (Bool -> Bool) is of class Prop, then so too is Bool -> (Bool -> Bool). I could be mistake, but I'm fairly sure that Bool -> Bool -> Bool is actually just short-hand for this. So this means that a boolean function of two boolean variables is itself a proposition. How do we determine its validity? We check if both f True and f False are valid. The former means 'if f True False and f True True both evaluate to True'.

Hopefully you can see now the recursion that's going on (I haven't done a great job explaining it; sorry)-- what we're doing is recursively defining the validity of the type Bool -> Bool -> .... -> Bool so that such a function is valid if and only if it evaluates to True for all possible inputs.

• XXX: You have masterfully avoided going in the detail of the only line of code you have really changed from my question to your answer :)
• Myridium: @Boris - Sorry, which line is that? Apart from a typo I corrected, I don't recall there being any differences.
• XXX: You explained everything that the textbook explained, and left answering my question as exercise :)
• Myridium: @Boris - I added a bit to Inductive Instance Definition - First Step.
• Myridium: @Boris - If I had more time, I would have written a shorter answer. Thank you for the question; I've since built upon the example and added operators like ==> and the forall and exists quantifiers acting on enumerable sets of propositions.