Boolean Evaluation
Contents
Boolean Evaluation¶
Representing Expressions¶
Using Natural Deduction, we could prove arguments like \((A \implies B) \therefore (\neg A \vee B)\). Natural Deduction is a very nice method for humans to use. Computer base approaches tend to be based more around truth tables. These are much easier to program.
Every deductive argument can be rewritten into a Truth Table problem. We will look at the following argument.
\( \begin{align} \neg X, A \implies B, B \implies X \therefore \neg(A \vee B) \end{align} \)
We can rewrite any argument as just a conclusion. First, we can replace the commas with conjunctions. Since we can always use \(\wedge E\) to take a long conjunction apart and make all the individual premises.
\( \begin{align} \left( (\neg X) \wedge (A \implies B) \wedge (B \implies X) \right) \therefore \neg(A \vee B) \end{align} \)
This is harder to read, but it conveys the same information. Next, the therefore (\(\therefore\)) is just telling us that if the premises are true then the conclusion will be. We can just make that into an implies conclusion.
\( \begin{align} \therefore \left( \left( (\neg X) \wedge (A \implies B) \wedge (B \implies X) \right) \implies \neg(A \vee B) \right) \end{align} \)
This argument is exactly the same as the original argument. In this case, we are verifying that this expression is a tautology. If it is, the original argument was true. This format is normally much harder for humans to read, but it is much nicer for a computer. The computer only gets a conclusion and always has the same goal, show a tautology.
We can still solve this in the proof checker. The proof becomes very messy.
A computer won’t have to worry about this, since it will just be focused on how the expression evaluates.
Boolean Operators¶
To avoid confusion with Racket syntax, we will use custom names for all our expressions.
Function Template |
Meaning |
|---|---|
|
\(A \wedge B\) |
|
\(A \vee B\) |
|
\(\neg A\) |
|
\(A \implies B\) |
|
\(A \iff B\) |
We can write expressions using this notation. They don’t mean anything to Racket. As far as Racket is concerned, this is just a list. We will have to give it a meaning.
(define exp1 '(<-> (v (~ A) B) (-> A B)) )
(define exp2 '(-> (& A B) B) )
These expressions are both tautologies. Written in classic notation they are given below.
\( \begin{align} (\neg A \vee B) \iff& (A \implies B) \\ (A \wedge B) \implies& B \end{align} \)
We want to ask Racket to prove these statements for us.
Environments¶
If we want to evaluate an expression, we need to know what the variables are set to. For example, we should be able to ask “Is my expression true when A is true and B is false. This is a purely mechanical process. We just need to know what the expression means and the variable settings.
A collection of variable settings is called an environment. In Racket, all an environment is is a list of variables and their values.
Imagine you had a simple function like
(define (f a b)
(* a b)
)
We might then call (f 5 2). What we are telling racket is to make an environment with \(a=5\) and \(b=2\). Then evaluate the function body.
The environment just looks like a list.
'((a 5) (b 2))
Racket even has a command called let that allows us to create environments as we need them.
(let
((a 5) (b 7))
(* a b)
)
When we want to provide the settings for our variables, we need to create an environment.
For example, we could say A=true and B=false by creating
(define env1 '( (A true) (B false) ) )
We again use special symbols true and false instead of the Racket commands #t and #f. This will make our expression and code stand out more distinctly. Remember, we want to build a system to answer our questions about the boolean expressions. We don’t just want to let Racket evaluate an expression.
Once we have an environment, we might need to look up values in it.
There are three conditions related to looking for variables.
The environment is empty
We found it!
We didn’t find it yet, but need to keep looking.
If the environment is null, then it is hopeless to find anything. There is nowhere to look. We can cause an error in this situation. To create an error in Racket, we use the raise command.
We also need to think about where our information appears in the list. The first element of the first list is the name of the variable. The second element of the second list is the value.
(define (getFirstVar env)
(first (first env))
)
(define (getFirstVal env)
(second (first env))
)
If the first variable is not the one we want, we just need to look at the rest of the list.
The full function to get the value of a target variable is given below.
(define (getValue target env)
(cond
;The environment is empty
[(null? env) (raise "Variable not found.")]
;We found it!
[(equal? target (getFirstVar env))
(getFirstVal env)]
;We need to keep looking
[else (getValue target (rest env))]
)
)
We can test this on the environment we defined earlier.
(getValue 'A env1) ; true
(getValue 'B env1) ; false
(getValue 'C env1) ;Throws error
At this point, we have a way to write Boolean expressions and a way to define what value each variable has. We need a way to evaluate an expression with a set of variables, then we can decide if it is true or false.
Evaluation¶
To write an evaluator, we need to detect what type of expression we are looking at.
A Negation is a list with 2 items in it. The first item is the negation symbol we have chosen. The second is the expression it is being applied to.
(define (isNot? expr)
(and
(list? expr)
(equal? (length expr) 2)
(equal? '~ (first expr))
)
)
All the other operators are binary. That means they are lists of length 3. The first item is the operator. The other two items in the list are the inputs. We can make a general comparison for any operator and length.
(define (isOperator op len)
(lambda (expr)
(and
(list? expr)
(equal? (length expr) len)
(equal? op (first expr))
)
)
)
Then define all our special cases using this one function.
(define isNot? (isOperator '~ 2) )
(define isAnd? (isOperator '& 3) )
(define isOr? (isOperator 'v 3) )
(define isImplies? (isOperator '-> 3))
(define isBicond? (isOperator '<-> 3))
To evaluate an expression, we need to determine what type of expression it is. Then follow the correct instructions. The evaluate function needs an expression to evaluate and an environment with the variable settings.
The evaluate function has many conditions, but they are all short. There are two constants, we do nothing with them. Then we check for each operator. For each operator, we will just write a function explaining how it works. Lastly, if the input is “none of the above” we will treat it as a variable. We will assume it is defined in the environment and look it up.
(define (evaluateExp exp env)
(cond
;Constants don't do anything
[(equal? exp 'true) 'true]
[(equal? exp 'false) 'false]
;Evaluate the Operators
[(isNot? exp) (evalNot exp env)]
[(isAnd? exp) (evalAnd exp env)]
[(isOr? exp) (evalOr exp env)]
[(isImplies? exp) (evalImplies exp env)]
[(isBicond? exp) (evalBicond exp env)]
;Anything else must be a variable
[else (getValue exp env)]
)
)
We need to describe how each operator works. Each operator takes either one operand or two operands. We make two functions to easily get them out.
(define (op1 exp)
(second exp)
)
(define (op2 exp)
(third exp)
)
To evaluate a negation, we evaluate the first operand. If it evaluates to true, we return false. Otherwise, we return true.
(define (evalNot exp env)
(if (equal? 'true (evaluateExp (op1 exp) env))
'false
'true
)
)
To evaluate a conjunction, we need to evaluate the first operand. If the first operand evaluates to false, then the expression is false. The second operand doesn’t matter at all if the first is false. If the first operand it true, then the second operand decides the result.
(define (evalAnd exp env)
(if (equal? 'true (evaluateExp (op1 exp) env))
(evaluateExp (op2 exp) env)
'false
)
)
For a disjunction, if the first operand evaluates to true then the whole expression is true. Otherwise, the result is decided by the second operand.
(define (evalOr exp env)
(if (equal? 'true (evaluateExp (op1 exp) env))
'true
(evaluateExp (op2 exp) env)
)
)
A conditional statement is always true if the first operand is false. Otherwise, the result is whatever the second operand evaluates to.
(define (evalImplies exp env)
(if (equal? 'true (evaluateExp (op1 exp) env))
(evaluateExp (op2 exp) env)
'true
)
)
The bi-conditional is the most complex. Neither operand has a short-cut. If the first operand is true, then we also need to evaluate the second one to see if it is true. Likewise, if the first operand is true, then we care that the second if false.
(define (evalBicond exp env)
(if (equal? 'true (evaluateExp (op1 exp) env))
(evaluateExp (op2 exp) env)
(if (equal? 'true (evaluateExp (op2 exp) env)) 'false 'true)
)
)
We can use this to evaluate general expressions.
We can get all the results for the conditional.
(display "Make Truth Table for Implies\n")
(evaluateExp '(-> A B) '( (A true) (B true)) ) ;true
(evaluateExp '(-> A B) '( (A true) (B false)) );false
(evaluateExp '(-> A B) '( (A false) (B true)) );true
(evaluateExp '(-> A B) '( (A false) (B false)));true
We can even evaluate the expression we wrote at the beginning of this section.
(display "Make Truth Table for exp1\n")
(evaluateExp exp1 '( (A true) (B true)) ) ;true
(evaluateExp exp1 '( (A true) (B false)) );true
(evaluateExp exp1 '( (A false) (B true)) );true
(evaluateExp exp1 '( (A false) (B false)));true
We can evaluate exp2 from earlier easily as well.
(display "Make Truth Table for exp2\n")
(evaluateExp exp2 '( (A true) (B true)) ) ;true
(evaluateExp exp2 '( (A true) (B false)) );true
(evaluateExp exp2 '( (A false) (B true)) );true
(evaluateExp exp2 '( (A false) (B false)));true
Tautology Checker¶
If we want to check if something is a tautology, we need to evaluate it on every row of the truth table. We make the input columns for a two variable truth table.
(define twoColTT '(
((A true) (B true))
((A true) (B false))
((A false) (B true))
((A false) (B false))
)
)
We can map evaluation over every one of these environments.
(define (evaluateTT exp TT)
(map (lambda (e) (evaluateExp exp e)) TT)
)
This gets us the whole truth table result column in just one command.
(evaluateTT '(& A B) twoColTT) ;'(true false false false)
To decide if the expression is a tautology, we just need to make sure every value is a true. We can complete this with a foldr.
(define (andAll resultCol)
(foldr
;Implementation of a /\ b
(lambda (a b) (if (equal? a 'true) b 'false))
'true ;Initial Value
resultCol;Result column of the truth table
)
)
We can ask if something is a tautology. This only works for two variables, but we could programmatically generate the truth table inputs as well.
(define (isTautology exp inputTT)
(andAll (evaluateTT exp inputTT)))
We prove that \(\neg A \vee A\) is a tautology.
(define oneColTT '(
((A true))
((A false))
)
)
(isTautology '(v (~ A) A) oneColTT) ;'true
We prove some additional arguments.
;Additional Examples
;Implies Definition
(isTautology '(<-> (v (~ A) B) (-> A B) )twoColTT);true
;Demorgan's Laws
(isTautology '(<-> (~ (& A B)) (v (~ A) (~ B))) twoColTT) ;true
(isTautology '(<-> (~ (v A B)) (& (~ A) (~ B))) twoColTT) ;true
We can even prove the following argument as long as we make a bigger truth table.
\( \begin{align} \therefore \left( \left( (\neg X) \wedge (A \implies B) \wedge (B \implies X) \right) \implies \neg(A \vee B) \right) \end{align} \)
(define threeColTT
'(
( (A true) (B true) (X true) )
( (A true) (B true) (X false) )
( (A true) (B false) (X true) )
( (A true) (B false) (X false) )
( (A false) (B true) (X true) )
( (A false) (B true) (X false) )
( (A false) (B false) (X true) )
( (A false) (B false) (X false) )
)
)
(isTautology
;Expression
'(-> (& (& (~ X) (-> A B)) (-> B X)) (~ (v A B)))
;Truth Table Inputs
threeColTT
); returns True
Building a program to do our proofs for us requires fully understanding both the boolean logic we are working with a list processing to manipulate the symbolic expressions.
Full Source Code¶
A completed version of the source code with comments is provided below.
#lang racket
;Mark Boady
;Drexel University
;Given an expression and a
;table of boolean inputs
;determine if the expression is a tautology
;------------------------------------------------
;Section 1: Working with the environment
;------------------------------------------------
;Get the first variable out of an environment
;input-contract: (list? env)
;output-contract: (symbol? (getFirstVal env))
(define (getFirstVar env)
(first (first env))
)
;Get the first value out of an environment
;input-contract: (list? env)
;output-contract: (or (equal? (getFirstVal env) 'true)
; (equal? (getFirstVal env) 'false))
(define (getFirstVal env)
(second (first env))
)
;Search the Environment for a target variable
;return the value related to that variable name
;input-contract: (and (symbol? target) (list? env))
;output-contact: (or (equal? (getValue target env) 'true)
; (equal? (getValue target env) 'false))
;Throws an error if target not found
(define (getValue target env)
(cond
;The environment is empty
[(null? env) (raise "Variable not found.")]
;We found it!
[(equal? target (getFirstVar env))
(getFirstVal env)]
;We need to keep looking
[else (getValue target (rest env))]
)
)
;------------------------------------------------
;Section 2: Predicates
;------------------------------------------------
;Detect Expression Type
;Given an operator and list length
;creates a procedure to detect expressions of that format
;input-contract: (and (symbol? op) (integer? len))
;output-contract: (procedure? (isOperator op len))
(define (isOperator op len)
(lambda (expr)
(and
(list? expr)
(equal? (length expr) len)
(equal? op (first expr))
)
)
)
;Define the formats we need
;Negation only takes 1 input
;Other Boolean Operators are 2 inputs and the operator
(define isNot? (isOperator '~ 2) )
(define isAnd? (isOperator '& 3) )
(define isOr? (isOperator 'v 3) )
(define isImplies? (isOperator '-> 3))
(define isBicond? (isOperator '<-> 3))
;------------------------------------------------
;Section 3: Evaluate An Expression
;------------------------------------------------
;Get the first operand of an expression
;input-contract: A valid expression
;output-contact: The first operand
(define (op1 exp)
(second exp)
)
;Get the second operand of an expression
;input-contract: A valid expression
;output-contact: The second operand
(define (op2 exp)
(third exp)
)
;Evaluate a Negation statement
;input-contract: A negation expression and environment
;output-contract: true/false based on expression and env
(define (evalNot exp env)
(if (equal? 'true (evaluateExp (op1 exp) env))
'false
'true
)
)
;Evaluate a Conjunction statement
;input-contract: A conjunction expression and environment
;output-contract: true/false based on expression and env
(define (evalAnd exp env)
(if (equal? 'true (evaluateExp (op1 exp) env))
(evaluateExp (op2 exp) env)
'false
)
)
;Evaluate a disjuction statement
;input-contract: A disjunction expression and environment
;output-contract: true/false based on expression and env
(define (evalOr exp env)
(if (equal? 'true (evaluateExp (op1 exp) env))
'true
(evaluateExp (op2 exp) env)
)
)
;Evaluate a Conditional statement
;input-contract: A conditional expression and environment
;output-contract: true/false based on expression and env
(define (evalImplies exp env)
(if (equal? 'true (evaluateExp (op1 exp) env))
(evaluateExp (op2 exp) env)
'true
)
)
;Evaluate a Bi-conditional statement
;input-contract: A bi-conditional expression and environment
;output-contract: true/false based on expression and env
(define (evalBicond exp env)
(if (equal? 'true (evaluateExp (op1 exp) env))
(evaluateExp (op2 exp) env)
(if (equal? 'true (evaluateExp (op2 exp) env)) 'false 'true)
)
)
;Evaluate an expression on a given environment
;input-contract: A valid expression and environment
;output-contract: true/false based on expression
(define (evaluateExp exp env)
(cond
;Constants don't do anything
[(equal? exp 'true) 'true]
[(equal? exp 'false) 'false]
;Evaluate the Operators
[(isNot? exp) (evalNot exp env)]
[(isAnd? exp) (evalAnd exp env)]
[(isOr? exp) (evalOr exp env)]
[(isImplies? exp) (evalImplies exp env)]
[(isBicond? exp) (evalBicond exp env)]
;Anything else must be a variable
[else (getValue exp env)]
)
)
;------------------------------------------------
;Section 4: Tautology Checker
;------------------------------------------------
;Evaluate and expression on
;every environment in a truth table
;input-contract: a valid boolean expression and truth table
;output-contract: a list of true/false values
(define (evaluateTT exp TT)
(map (lambda (e) (evaluateExp exp e)) TT)
)
;And all the true/false values in a list
;input-contract: a list containing only true/false
;output-contract: true or false
;returns true if all values in the list are true
(define (andAll resultCol)
(foldr
;Implementation of a /\ b
(lambda (a b) (if (equal? a 'true) b 'false))
'true ;Initial Value
resultCol;Result column of the truth table
)
)
;Tautology Checker
;Evaluates expression on truth table
;and makes sure all results are true
;input-contract: a valid expression and table table inputs
;output-contract: true if the expression is a tautology
; and false otherwise
(define (isTautology exp inputTT)
(andAll (evaluateTT exp inputTT)))
;------------------------------------------------
;Section 5: Experiments
;------------------------------------------------
;Define two expression to test with
(define exp1 '(<-> (v (~ A) B) (-> A B)) )
(define exp2 '(-> (& A B) B) )
;Define an environment
(define env1 '( (A true) (B false) ) )
;Check that we can look up variables
(display "Environment Lookup Tests\n")
(getValue 'A env1) ; true
(getValue 'B env1) ; false
;This will throw and error if uncommented
;(getValue 'C env1) ;Throws error
;Evaluate Expressions
;Truth Tables for Common Operators
(display "Make Truth Table for Not\n")
(evaluateExp '(~ A) '( (A true)) ) ;true
(evaluateExp '(~ A) '( (A false)) );false
(display "Make Truth Table for And\n")
(evaluateExp '(& A B) '( (A true) (B true)) ) ;true
(evaluateExp '(& A B) '( (A true) (B false)) );false
(evaluateExp '(& A B) '( (A false) (B true)) );false
(evaluateExp '(& A B) '( (A false) (B false)));false
(display "Make Truth Table for Or\n")
(evaluateExp '(v A B) '( (A true) (B true)) ) ;true
(evaluateExp '(v A B) '( (A true) (B false)) );true
(evaluateExp '(v A B) '( (A false) (B true)) );true
(evaluateExp '(v A B) '( (A false) (B false)));false
(display "Make Truth Table for Implies\n")
(evaluateExp '(-> A B) '( (A true) (B true)) ) ;true
(evaluateExp '(-> A B) '( (A true) (B false)) );false
(evaluateExp '(-> A B) '( (A false) (B true)) );true
(evaluateExp '(-> A B) '( (A false) (B false)));true
(display "Make Truth Table for Biconditional\n")
(evaluateExp '(<-> A B) '( (A true) (B true)) ) ;true
(evaluateExp '(<-> A B) '( (A true) (B false)) );false
(evaluateExp '(<-> A B) '( (A false) (B true)) );false
(evaluateExp '(<-> A B) '( (A false) (B false)));true
;Truth Tables for example Expressions
(display "Make Truth Table for exp1\n")
(evaluateExp exp1 '( (A true) (B true)) ) ;true
(evaluateExp exp1 '( (A true) (B false)) );true
(evaluateExp exp1 '( (A false) (B true)) );true
(evaluateExp exp1 '( (A false) (B false)));true
(display "Make Truth Table for exp2\n")
(evaluateExp exp2 '( (A true) (B true)) ) ;true
(evaluateExp exp2 '( (A true) (B false)) );true
(evaluateExp exp2 '( (A false) (B true)) );true
(evaluateExp exp2 '( (A false) (B false)));true
;Define Truth Tables
(define oneColTT '(
((A true))
((A false))
)
)
(define twoColTT '(
((A true) (B true))
((A true) (B false))
((A false) (B true))
((A false) (B false))
)
)
(define threeColTT
'(
( (A true) (B true) (X true) )
( (A true) (B true) (X false) )
( (A true) (B false) (X true) )
( (A true) (B false) (X false) )
( (A false) (B true) (X true) )
( (A false) (B true) (X false) )
( (A false) (B false) (X true) )
( (A false) (B false) (X false) )
)
)
;Test Evaluate TT
(display "Example of evaluateTT Mapping an Expression\n")
(evaluateTT '(& A B) twoColTT)
(display "Tautology Verifictions\n")
;Verify Tautologies
;~A or A
(isTautology '(v (~ A) A) oneColTT) ;'true
;Implies Definition
(isTautology '(<-> (v (~ A) B) (-> A B) )twoColTT);true
;Demorgan's Laws
(isTautology '(<-> (~ (& A B)) (v (~ A) (~ B))) twoColTT) ;true
(isTautology '(<-> (~ (v A B)) (& (~ A) (~ B))) twoColTT) ;true
(isTautology
;Expression
'(-> (& (& (~ X) (-> A B)) (-> B X)) (~ (v A B)))
;Truth Table Inputs
threeColTT
); returns True
The full output is provided below.
Welcome to DrRacket, version 8.0 [cs].
Language: racket, with debugging; memory limit: 256 MB.
Environment Lookup Tests
'true
'false
Make Truth Table for Not
'false
'true
Make Truth Table for And
'true
'false
'false
'false
Make Truth Table for Or
'true
'true
'true
'false
Make Truth Table for Implies
'true
'false
'true
'true
Make Truth Table for Biconditional
'true
'false
'false
'true
Make Truth Table for exp1
'true
'true
'true
'true
Make Truth Table for exp2
'true
'true
'true
'true
Example of evaluateTT Mapping an Expression
'(true false false false)
Tautology Verifictions
'true
'true
'true
'true
'true