Verifying tautologies with Haskell

< change language

A tautology is a formula that is true regardless of the logical value we attribute to the variables it contains. For example, the propositional formula $P \vee \neg P$ is always true, regardless of $P$ being true or false. But not every tautology is as simple as the one I just showed. For example, showing that $$(P \implies Q) \implies [(Q \implies R) \implies (P \implies R)]$$ is a tautology requires a bit more thought. But thinking is too tiring, so let us write a Haskell program that takes a formula and decides if the formula is a tautology or not! (By the way, said program is available in my GitHub...) First we need to be able to represent a proposition and we will create a data type just for that. We will call our type "Prop", from proposition, from propositional logic. where we provided data constructors for all sorts of propositional formulas. The idea is that now the formula $P \vee \neg P$ is represented as Or (Var "P") (Neg (Var "P")).

Now we have a way of representing formulas. What we are left with is having a way of evaluating those formulas to check if they are tautologies... Propositions will have variables, so we will need to collect the variables of a proposition, generate all possible combinations of values to attribute to all the variables, and then evaluate the logical value of the proposition with the given attribution. Notice that most of our functions will make use of the structure of the data Prop in order to do some sort of "recursion", but on the structure of the proposition. For example, if you have a proposition p = Or p1 p2 then the variables in $p$ are the variables in $p_1$ concatenated with the variables in $p_2$. Now that we have all variables, we can generate all the possible combinations of values they can take. If we only have one variable, that is $T, F$. If we have two variables, that's $TT$, $TF$, $FT$, $FF$. If we have three variables, ... I define the function that generates all possible combinations of true/false values and then put them together with our variables. And now that we can define attributions for our variables, we can write a function that takes a proposition and an attribution, and evaluates the proposition according to the attribution! Our function will have signature Prop -> Attribution -> Maybe Bool because we cannot know for sure that the attribution that is passed in contains all the variables present in the proposition. We are very close to the finish line! Given a proposition $p$, how do we check if it is a tautology? Well, we should generate all of the possible attributions for it, evaluate each one of them, and check if all the attributions made the proposition true! And that is exactly what we do in the next few lines: Now that our program is written down, we can actually check some tautologies!

We will check the tautology I presented in the beginning and three more tautologies: the definitions of "and", "or" and "equivalent" in terms of the negation and implication. That is, $P \vee Q$, $P \wedge Q$ and $P \iff Q$ can be written down only using negations and implications, and I will use this program to check that! And obviously this will print "True" four times.
In my GitHub page you can find this program with two extra functions, falsify and truthify that try to find an attribution that makes the given proposition evaluate to false/true.

If you liked this post, consider subscribing to the Mathspp newsletter and like it on Facebook.

Uma tautologia é uma fórmula lógica que é verdadeira independentemente do valor lógico que as suas variáveis tomam. Por exemplo, a fórmula proposicional $P \vee \neg P$ é uma tautologia porque independentemente de $P$ ser verdadeiro ou falso, a fórmula tem sempre o valor de "verdadeiro". Mas nem todas as tautologias são tão simples quanto esta que acabei de mostrar. Por exemplo, $$(P \implies Q) \implies [(Q \implies R) \implies (P \implies R)]$$ também é uma tautologia e já não é completamente óbvio porquê. Claro que podemos raciocinar sobre o assunto, mas pensar dá demasiado trabalho. Vamos antes escrever um programa em Haskell que verifique se uma fórmula é uma tautologia! (O código do programa que vamos ver agora está no meu GitHub...) Primeiro vamos ter que arranjar uma maneira de representar proposições lógicas, e para isso vamos criar um tipo novo. Vamos chamar "Prop" ao nosso tipo, de "proposição" lógica. os construtores disponíveis servem para construir os vários tipos de fórmulas. A ideia é que a fórmula $P \vee \neg P$ agora seja representada por Or (Var "P") (Neg (Var "P")).

Agora já temos uma forma de representar fórmulas; só falta saber avaliá-las! As proposições, em geral, têm variáveis. Vamos ter de encontrar todas as variáveis numa proposição e depois vamos ter de gerar todas as possíveis combinações de valores que essas variáveis podiam tomar, e depois vamos ter de avaliar a proposição em cada um desses casos. Repare-se também que a maior parte das funções que vamos definir vão estar definidas por recursão na estrutura do tipo Prop; isto é, as funções vão "desconstruindo" as proposições e operando em proposições mais pequenas. A título de exemplo, se tivermos uma proposição p = Or p1 p2 então as variáveis que aparecem na proposição $p$ são a união das variáveis em $p_1$ e em $p_2$. Já sabemos colecionar todas as variáveis de uma proposição e já estamos em posição de gerar todas as combinações de valores possíveis. Se só tivermos uma variável, então as combinações todas são só $V$ e $F$; se tivermos duas variáveis, as combinações são $VV$, $VF$, $FV$, $FF$; se tivermos três variáveis, ... Aqui está definida uma função que gera todas as combinações e outra função que junta cada valor a cada variável. Agora que já sabemos definir as atribuições para as nossas variáveis, só falta haver uma função que recebe uma proposição e uma atribuição das suas variáveis, e que devolve o valor lógico da proposição segundo essa atribuição. A função vai ter tipo Prop -> Attribution -> Maybe Bool porque, à partida, não sabemos se a proposição vai ter variáveis que não são contempladas na atribuição. Estamos quase no fim! Dada uma proposição $p$, como podemos saber se ela é uma tautologia? Temos de gerar todas as atribuições possíveis, avaliar a proposição com cada uma delas, e ver se o valor lógico deu "verdadeiro" para todas as avaliações! E é exatamente isso que fazemos nas próximas linhas de código: Agora que o programa está escrito podemos testar algumas tautologias.

Vamos verificar a tautologia que apresentei no início e outras três: as definições das operações "e", "ou" e "equivalente" em termos de negações e implicações. Ou seja, estou a afirmar que $P \vee Q$, $P \wedge Q$ e $P \iff Q$ podem ser definidos usando apenas negações e implicações e claro que vou usar este programa para verificar isso! Se corrermos a função main vamos ver "True" na consola quatro vezes.
Podem encontrar este programa na minha página do GitHub; o programa tem duas funções extra, falsify e truthify, que recebem uma proposição e tentam encontrar uma atribuição que torne a proposição falsa (respetivamente verdadeira).

Se gostaram deste post, considerem subscrever a newsletter do blog e deixem um like no Facebook.

  - RGS