Brontekst bekijken van Beweren en bewijzen/de zuilen/Taal/3. Syntax en semantiek/latex

%<noinclude><source lang="tex">

\documentclass[a4paper,12pt]{article}
\usepackage[english,dutch]{babel}

\usepackage{a4wide}
\pagestyle{empty}

\newcommand{\forget}[1]{\addtolength{\textheight}{#1}\setlength{#1}{0pt}}
\forget{\headheight}
\forget{\headsep}
\forget{\footskip}

\usepackage{amssymb, amsmath}
\usepackage[dutch,english]{babel}
\selectlanguage{dutch}

\renewcommand{\implies}{\rightarrow}
\renewcommand{\impliedby}{\leftarrow}
\renewcommand{\iff}{\leftrightarrow}

\newcommand{\vb}[1]{\fbox{\scriptsize $#1$}}
\newcommand{\tp}[1]{$^{\,#1}$}
\newcommand{\ra}{\rightarrow}
\newcommand{\alt}{|}
\newcommand{\Alt}{{\bf\ \ \ $|$ \ \ }}
\newcommand{\nat}{{\mathbb{N}}}
\newcommand{\zed}{{\mathbb{Z}}}
\newcommand{\bew}{{\mathbb{B}}}
\newcommand{\real}{{\mathbb{R}}}
\newcommand{\lit}[1]{\textup{\textsf{#1}}}


\begin{document}

\subsection*{Grammatica \tiny{(versie 30/06/14)}} Legenda:
De letters $\sigma$ en $\tau$ worden gebruikt om willekeurige types aan te geven.
De letter $\rho$ wordt specifiek gebruikt om $\zed$ of $\real$ aan te geven. \\
\textsf{\textit{formule}}\tp{\bew\alt\tau} genereert formules van type $\bew$, en via een tweede alternatief (meer) formules van type $\tau$.\\
\begin{sffamily}
\begin{itshape}
\begin{tabular}{ll}
sectie & naamgeving sectie \Alt naamgeving \\
naamgeving & \lit{Variable} naam\tp{\tau} \lit{:} type\tp{\tau} \lit{.} \hfill \textrm{een punt ter afsluiting}\\
& \Alt \lit{Definition} naam\tp{\tau} abstractie\tp{\tau} \lit{.} \\
& \Alt \lit{Theorem} naam\tp{\bew} \lit{:} formule\tp{\bew} \lit{.} \\
&\qquad \vb{\mathsf{Variable}\;\mathit{neerslag}: R.}
\\
&\qquad \vb{\mathsf{Variable}\;\mathit{Mens}: \mathsf{Set}.} \hfill \textrm{maakt een nieuw type `Mens'}
\\
&\qquad \vb{\mathsf{Variable}\;\mathit{BSN}: \mathit{Mens}\ra\mathit{Z}.}
\\
&\qquad \vb{\mathsf{Definition}\;P\;(m:Z)\;:= \neg(\exists p:Z, 1<p \land p<m \land (\exists q:Z, m=p\times q)).}
\smallskip\\
abstractie\tp{\tau\alt\sigma\ra\tau} & \lit{:=} formule\tp{\tau} \Alt parameter\tp{\sigma} abstractie\tp{\tau}\\
parameter\tp{\tau} & \lit{(} naam\tp{\tau} \lit{:} type\tp{\tau} \lit{)} \smallskip\\
\hline
formule\tp{\bew\alt\tau} & kwantor naam\tp{\sigma} \lit{:} type\tp{\sigma} \lit{,} formule\tp{\bew} 
\Alt equivalentie\tp{\tau} \rule{0pt}{\bigskipamount}\\
&\qquad \vb{\forall m:Z, P\;m \implies (\exists n:Z, P\;n \land m<n)}
\smallskip\\
& \hfill \textrm{een komma in plaats van de gebruikelijke punt}\\
equivalentie\tp{\bew\alt\tau} & equivalentie\tp{\bew} $\iff$ implicatie\tp{\bew} \Alt implicatie\tp{\tau} \\
&\qquad \vb{x \land y \iff \neg x \land \neg y}
\smallskip\\
implicatie\tp{\bew\alt\tau} & disjunctie\tp{\bew} $\implies$ implicatie\tp{\bew} \Alt disjunctie\tp{\tau} \\
&\qquad \vb{a \implies b \implies a}
\\
disjunctie\tp{\bew\alt\tau} & conjunctie\tp{\bew} $\lor$ disjunctie\tp{\bew} \Alt conjunctie\tp{\tau}\\
&\qquad \vb{p \land \neg q \lor \neg p \land q}
\smallskip\\
conjunctie\tp{\bew\alt\tau} & negatie\tp{\bew} $\land$ conjunctie\tp{\bew} \Alt negatie\tp{\tau} \\
negatie\tp{\bew\alt\tau} & $\neg$ negatie\tp{\bew} \Alt vergelijking\tp{\tau} \\
&\qquad \vb{\neg(\forall n:Z, P\;n \implies P\;(n{+}2))}
\smallskip\\
\hline
vergelijking\tp{\bew\alt\tau} & som\tp{\tau} gelijkongelijk som\tp{\tau} \Alt som\tp{\rho} kleinergelijkgroter som\tp{\rho} \rule{0pt}{\bigskipamount} \\
& \Alt som\tp{\rho} $\in$ interval\tp{\mathcal{P}(\rho)} \Alt som\tp{\tau} \hfill \textrm{met $\rho\in\{\zed,\real\}$}\\
&\qquad \vb{a\times(x+2) + b\times x + c = 0}
\smallskip\\
interval\tp{\mathcal{P}(\rho)} & \lit{[} som\tp{\rho} \lit{,} som\tp{\rho} \lit{]} \Alt \lit{[} som\tp{\rho} \lit{,} som\tp{\rho} \lit{)} \\
& \Alt \lit{(} som\tp{\rho} \lit{,} som\tp{\rho} \lit{]} \Alt \lit{(} som\tp{\rho} \lit{,} som\tp{\rho} \lit{)} \hfill \textrm{met $\rho\in\{\zed,\real\}$}
\\
som\tp{\rho\alt\tau} & som\tp{\rho} plusminus product\tp{\rho} \Alt product\tp{\tau} \hfill \textrm{met $\rho\in\{\zed,\real\}$}\\
product\tp{\rho\alt\tau} & product\tp{\rho} maaldoor negatief\tp{\rho} \Alt negatief\tp{\tau} \qquad\hfill \textrm{met $\rho\in\{\zed,\real\}$}\\
&\qquad \vb{(p+q) \times (p-q)}
\smallskip\\
negatief\tp{\rho\alt\tau} & $-$ negatief\tp{\rho} \Alt macht\tp{\tau} \hfill \textrm{met $\rho\in\{\zed,\real\}$} \\
&\qquad \vb{-5}
\smallskip\\
macht\tp{\rho\alt\tau} & term\tp{\rho} \^{} macht\tp{\nat} \Alt term\tp{\tau} \hfill \textrm{met $\rho\in\{\zed,\real\}$}\\
&\qquad \vb{2 $\^{}$ 2 $\^{}$ k}
\smallskip\\
\hline
term\tp{\tau} & term\tp{\sigma\ra\tau} waarde\tp{\sigma} \Alt waarde\tp{\tau} \rule{0pt}{\bigskipamount}\\
&\qquad \vb{\mathit{max}\;3\;m}
\vb{\mathit{Verkeerslicht\;linksaf\; groen}\;(\mathit{nu}{+}5)}
\smallskip\\
waarde\tp{\rho\alt\tau} & constante\tp{\rho} \Alt naam\tp{\tau} \Alt \lit{(} formule\tp{\tau} \lit{)} \\
\end{tabular}

\begin{tabular}{ll}
type\tp{\sigma\ra\tau \alt \tau} & basistype\tp{\sigma} $\ra$ type\tp{\tau} \Alt basistype\tp{\tau} \\
&\qquad \vb{Z\ra(Z\ra Z)\ra B}
\smallskip\\
basistype\tp{\bew\alt\zed\alt\real\alt\text{naam}\alt\tau} & \lit{B} \Alt \lit{Z} \Alt \lit{R} \Alt naam\tp{\mathsf{Set}} \Alt \lit{(} type\tp{\tau} \lit{)} \smallskip\\
&\qquad \vb{\mathit{Mens}} \vb{(\mathit{Mens} \ra Z)}
\smallskip\\
%& \hfill \textrm{`naam' is dus een zelf gemaakt type}\\
\hline
constante\tp{\rho} & $0\ldots9$ \Alt constante\tp{\rho} $0\ldots9$ \quad \hfill \textrm{met $\rho\in\{\zed,\real\}$}\rule{0pt}{\bigskipamount}\\
naam\tp{\tau} & eersteteken \Alt eersteteken etcetera\\
&\qquad \vb{\mathit{melk2S\_L\_A\_G\_R\_O\_O\_M}}
\\
etcetera & overigteken \Alt overigteken etcetera\\

eersteteken & $a\ldots z$ \Alt $A\ldots Z$ \Alt $\_$\\
overigteken & $a\ldots z$ \Alt $A\ldots Z$ \Alt $0\ldots 9$ \Alt $\_$ \Alt $'$\\

kwantor & $\forall$ \Alt $\exists$ \\
gelijkongelijk & $=$ \Alt $\neq$ \\
kleinergelijkgroter & $<$ \Alt $\leq$ \Alt $>$ \Alt $\geq$ \\
plusminus & $+$ \Alt $-$ \\
maaldoor & $\times$ \Alt $/$ \\
\end{tabular}

\end{itshape}
\end{sffamily}

\end{document}
%</source></noinclude>