10 The aim of this case study is twofold: it shows how to model boolean |
10 The aim of this case study is twofold: it shows how to model boolean |
11 expressions and some algorithms for manipulating them, and it demonstrates |
11 expressions and some algorithms for manipulating them, and it demonstrates |
12 the constructs introduced above.% |
12 the constructs introduced above.% |
13 \end{isamarkuptext}% |
13 \end{isamarkuptext}% |
14 % |
14 % |
15 \isamarkupsubsubsection{How Can We Model Boolean Expressions?% |
15 \isamarkupsubsubsection{Modelling Boolean Expressions% |
16 } |
16 } |
17 % |
17 % |
18 \begin{isamarkuptext}% |
18 \begin{isamarkuptext}% |
19 We want to represent boolean expressions built up from variables and |
19 We want to represent boolean expressions built up from variables and |
20 constants by negation and conjunction. The following datatype serves exactly |
20 constants by negation and conjunction. The following datatype serves exactly |
28 \isa{Const\ False}. Variables are represented by terms of the form |
28 \isa{Const\ False}. Variables are represented by terms of the form |
29 \isa{Var\ n}, where \isa{n} is a natural number (type \isa{nat}). |
29 \isa{Var\ n}, where \isa{n} is a natural number (type \isa{nat}). |
30 For example, the formula $P@0 \land \neg P@1$ is represented by the term |
30 For example, the formula $P@0 \land \neg P@1$ is represented by the term |
31 \isa{And\ {\isacharparenleft}Var\ {\isadigit{0}}{\isacharparenright}\ {\isacharparenleft}Neg\ {\isacharparenleft}Var\ {\isadigit{1}}{\isacharparenright}{\isacharparenright}}. |
31 \isa{And\ {\isacharparenleft}Var\ {\isadigit{0}}{\isacharparenright}\ {\isacharparenleft}Neg\ {\isacharparenleft}Var\ {\isadigit{1}}{\isacharparenright}{\isacharparenright}}. |
32 |
32 |
33 \subsubsection{What is the Value of a Boolean Expression?} |
33 \subsubsection{The Value of a Boolean Expression} |
34 |
34 |
35 The value of a boolean expression depends on the value of its variables. |
35 The value of a boolean expression depends on the value of its variables. |
36 Hence the function \isa{value} takes an additional parameter, an |
36 Hence the function \isa{value} takes an additional parameter, an |
37 \emph{environment} of type \isa{nat\ {\isasymRightarrow}\ bool}, which maps variables to their |
37 \emph{environment} of type \isa{nat\ {\isasymRightarrow}\ bool}, which maps variables to their |
38 values:% |
38 values:% |
62 {\isachardoublequote}valif\ {\isacharparenleft}CIF\ b{\isacharparenright}\ \ \ \ env\ {\isacharequal}\ b{\isachardoublequote}\isanewline |
62 {\isachardoublequote}valif\ {\isacharparenleft}CIF\ b{\isacharparenright}\ \ \ \ env\ {\isacharequal}\ b{\isachardoublequote}\isanewline |
63 {\isachardoublequote}valif\ {\isacharparenleft}VIF\ x{\isacharparenright}\ \ \ \ env\ {\isacharequal}\ env\ x{\isachardoublequote}\isanewline |
63 {\isachardoublequote}valif\ {\isacharparenleft}VIF\ x{\isacharparenright}\ \ \ \ env\ {\isacharequal}\ env\ x{\isachardoublequote}\isanewline |
64 {\isachardoublequote}valif\ {\isacharparenleft}IF\ b\ t\ e{\isacharparenright}\ env\ {\isacharequal}\ {\isacharparenleft}if\ valif\ b\ env\ then\ valif\ t\ env\isanewline |
64 {\isachardoublequote}valif\ {\isacharparenleft}IF\ b\ t\ e{\isacharparenright}\ env\ {\isacharequal}\ {\isacharparenleft}if\ valif\ b\ env\ then\ valif\ t\ env\isanewline |
65 \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ else\ valif\ e\ env{\isacharparenright}{\isachardoublequote}% |
65 \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ else\ valif\ e\ env{\isacharparenright}{\isachardoublequote}% |
66 \begin{isamarkuptext}% |
66 \begin{isamarkuptext}% |
67 \subsubsection{Transformation Into and of If-Expressions} |
67 \subsubsection{Converting Boolean and If-Expressions} |
68 |
68 |
69 \REMARK{is this the title you wanted?} |
|
70 The type \isa{boolex} is close to the customary representation of logical |
69 The type \isa{boolex} is close to the customary representation of logical |
71 formulae, whereas \isa{ifex} is designed for efficiency. It is easy to |
70 formulae, whereas \isa{ifex} is designed for efficiency. It is easy to |
72 translate from \isa{boolex} into \isa{ifex}:% |
71 translate from \isa{boolex} into \isa{ifex}:% |
73 \end{isamarkuptext}% |
72 \end{isamarkuptext}% |
74 \isacommand{consts}\ bool{\isadigit{2}}if\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}boolex\ {\isasymRightarrow}\ ifex{\isachardoublequote}\isanewline |
73 \isacommand{consts}\ bool{\isadigit{2}}if\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}boolex\ {\isasymRightarrow}\ ifex{\isachardoublequote}\isanewline |