1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
|
# CleanLogic
Logic toolbox in [Clean](http://wiki.clean.cs.ru.nl/Clean). Features include:
* Straightforward types for (atomic) expressions, operators and truth tables
* `toString` instances for all types that take care of associativity
* Substituting atomic expressions for constants
* Evaluating expressions without atomic expressions
* Generating truth tables for expressions, possibly with intermediate steps
* Displaying truth tables
Read further for examples.
## Types
### Operators
There is one unary operator (`Op1`): `Not`.
There are four binary operators (`Op2`): `And`, `Or`, `Impl` and `Equiv`. `And` is considered left-associative; all others are considered right-associative. Associativity is only important in `toString` functions. `Expr` itself is an unambiguous recursive type.
### Expressions
Expressions are constants (`B Bool`), atomic expressions (`Atom Char`), or applications of operators on other expressions (`App1 Op1 Expr` or `App2 Expr Op2 Expr`).
### Examples
// Some random examples
e1 = Atom 'p'
e2 = Atom 'q'
e3 = App1 Not e1
e4 = App2 e1 And e2
e5 = App2 e3 Or e2
e6 = App2 e3 Impl e3
e7 = App2 e4 Equiv e5
e8 = App2 (App2 (Atom 'p') And (Atom 'q')) Impl (Atom 'q')
e9 = App2 (Atom 'p') And (App2 (Atom 'q') Impl (Atom 'q'))
// To test associativity rules
e10 = App2 (App2 (Atom 'p') And (Atom 'q')) And (Atom 'r')
e11 = App2 (Atom 'p') And (App2 (Atom 'q') And (Atom 'r'))
e12 = App2 (App2 (Atom 'p') Or (Atom 'q')) Or (Atom 'r')
e13 = App2 (Atom 'p') Or (App2 (Atom 'q') Or (Atom 'r'))
e14 = App2 (App2 (Atom 'p') Impl (Atom 'q')) Impl (Atom 'r')
e15 = App2 (Atom 'p') Impl (App2 (Atom 'q') Impl (Atom 'r'))
e16 = App2 (App2 (Atom 'p') Equiv (Atom 'q')) Equiv (Atom 'r')
e17 = App2 (Atom 'p') Equiv (App2 (Atom 'q') Equiv (Atom 'r'))
## Substitution
You can substitute all occurences of `Atom a` in an `Expr e` by a `Bool b` with `substitute (a,b) e`. This yields a new `Expr`, in which all occurences have been replaced by the contstant `B b`.
An alternative is `substitute_all`, which takes a list of tuples `(a :: AtomName, b :: Bool)` and substitutes all atomnames with the corresponding booleans.
## Evaluation
An expression `e` **without atomic expressions** may be evaluated to its result by calling `eval e`. This yields the empty list `[]` if `e` *did* have atomic expressions, or a singleton `[b :: Bool]` with the result of the evaluation.
## Truth tables
A `TruthTable` has a list of expressions `exprs` and a list of `options`, which has the type `[[(AtomName,Bool)]]` and describes all the options the truth table should list.
A simple truth table of an expression `e` contains only the atomic expressions in `e` and `e` itself. It may be built with `simple_truthtable e`. A more complex truth table lists all `e`'s subexpressions. In either table, the expressions are roughly sorted by complexity.
A truth table `table` can be shown with `toString table`.
### Examples
The `simple_truthtable` of `e10`:
p | q | r | p & q & r
-------+-------+-------+-----------
False | False | False | False
False | False | True | False
False | True | False | False
False | True | True | False
True | False | False | False
True | False | True | False
True | True | False | False
True | True | True | True
The `truthtable` of `e15`:
p | q | r | q -> r | p -> q -> r
-------+-------+-------+--------+-------------
False | False | False | True | True
False | False | True | True | True
False | True | False | False | True
False | True | True | True | True
True | False | False | True | True
True | False | True | True | True
True | True | False | False | False
True | True | True | True | True
## Future ideas
* Different `toString` formats for operators: HTML (`¬`), UTF-8 (¬)
* Different `toString` formats for booleans: `0` and `1` or `T` and `F` instead of `True` and `False`
* Simplifying expressions with atomic expressions as far as possible
* Testing equivalence or impliance of expressions with atomic expressions
## License
This program and the example are distributed under the MIT license. For more details, see the LICENSE file.
|
