Skip to content

BOL semantics: add missing refl axiom for C_R* #132

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Closed
ComFreek wants to merge 1 commit into from
Closed

BOL semantics: add missing refl axiom for C_R* #132

Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
3 changes: 2 additions & 1 deletion WuV/bolsem.tex
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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.
Expand Down Expand Up @@ -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.
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.