diff --git a/WuV/bolsem.tex b/WuV/bolsem.tex index e11df03..74b9a4c 100644 --- a/WuV/bolsem.tex +++ b/WuV/bolsem.tex @@ -144,6 +144,7 @@ \subsection{Semantics} \begin{compactitem} \item A binary predicate symbol $C_R\sq i\times i$. Note that $R$ may be a complex expression; so we have to generate a fresh name $C_R$ here. \item The axiom $\forall x:\iota,y:\iota.\,R(x,y)\impl C_R(x,y)$, i.e., $C_R$ extends $R$. + \item The axiom $\forall x:\iota.\,C_R(x,x)$, i.e., $C_R$ is reflexive. \item The axiom $\forall x:\iota,y:\iota,z:\iota.\,C_R(x,y)\wedge C_R(y,z)\impl C_R(x,z)$, i.e., $C_R$ is transitive. \end{compactitem} \item We add the case $\sem{R^*}=C_R(x,y)$ to the interpretation function. @@ -625,4 +626,4 @@ \section{Exercise 2} You have to implement that as well or use a library for it. We recommend not focusing on implementing the syntax and semantics in their entirety. -It is more instructive to save time by choosing a sublanguage of BOL (by omitting some productions) and to use the time to implement a second semantics. \ No newline at end of file +It is more instructive to save time by choosing a sublanguage of BOL (by omitting some productions) and to use the time to implement a second semantics.