diff --git a/semester4/fmfp/formal-methods-functional-programming-summary.pdf b/semester4/fmfp/formal-methods-functional-programming-summary.pdf index cc1106e..8207692 100644 Binary files a/semester4/fmfp/formal-methods-functional-programming-summary.pdf and b/semester4/fmfp/formal-methods-functional-programming-summary.pdf differ diff --git a/semester4/fmfp/formal-methods-functional-programming-summary.tex b/semester4/fmfp/formal-methods-functional-programming-summary.tex index 3ee84e3..9b9aadf 100644 --- a/semester4/fmfp/formal-methods-functional-programming-summary.tex +++ b/semester4/fmfp/formal-methods-functional-programming-summary.tex @@ -28,6 +28,8 @@ \setup{Formal Methods \& Functional Programming} +% ──────────────────────────────────────────────────────────────────── + \begin{document} \startDocument @@ -59,6 +61,8 @@ \newpage \printtoc{Aquamarine} +% TODO: Strong and weak structural induction and more + \newsection \section{Haskell} @@ -66,85 +70,90 @@ \input{parts/00_haskell/01_syntax.tex} +\newsection +\section{Induction Proofs} +\input{parts/01_induction-proofs/00_intro.tex} +\input{parts/01_induction-proofs/01_mathematical-induction.tex} +\input{parts/01_induction-proofs/02_structural-induction.tex} +% \input{parts/01_induction-proofs/} + \newsection \section{Formal Reasoning} -\input{parts/01_formal-reasoning/00_formal-proofs.tex} -\input{parts/01_formal-reasoning/01_natural-deduction.tex} -\input{parts/01_formal-reasoning/02_propositional-logic/00_syntax.tex} -\input{parts/01_formal-reasoning/02_propositional-logic/01_semantics.tex} -\input{parts/01_formal-reasoning/02_propositional-logic/02_deductive-system.tex} -\input{parts/01_formal-reasoning/02_propositional-logic/03_natural-deduction-prop-logic.tex} -\input{parts/01_formal-reasoning/02_propositional-logic/04_derivation-rules-overview.tex} -\input{parts/01_formal-reasoning/03_first-order-logic/00_syntax.tex} -\input{parts/01_formal-reasoning/03_first-order-logic/01_semantics.tex} -\input{parts/01_formal-reasoning/03_first-order-logic/02_quantifiers.tex} -\input{parts/01_formal-reasoning/04_equality.tex} -\input{parts/01_formal-reasoning/05_correctness/00_intro.tex} -\input{parts/01_formal-reasoning/05_correctness/01_termination.tex} -\input{parts/01_formal-reasoning/05_correctness/02_behaviour.tex} -\input{parts/01_formal-reasoning/05_correctness/03_induction.tex} -% \input{parts/01_formal-reasoning/05_correctness/} -% \input{parts/01_formal-reasoning/} +\input{parts/02_formal-reasoning/00_formal-proofs.tex} +\input{parts/02_formal-reasoning/01_natural-deduction.tex} +\input{parts/02_formal-reasoning/02_propositional-logic/00_syntax.tex} +\input{parts/02_formal-reasoning/02_propositional-logic/01_semantics.tex} +\input{parts/02_formal-reasoning/02_propositional-logic/02_deductive-system.tex} +\input{parts/02_formal-reasoning/02_propositional-logic/03_natural-deduction-prop-logic.tex} +\input{parts/02_formal-reasoning/02_propositional-logic/04_derivation-rules-overview.tex} +\input{parts/02_formal-reasoning/03_first-order-logic/00_syntax.tex} +\input{parts/02_formal-reasoning/03_first-order-logic/01_semantics.tex} +\input{parts/02_formal-reasoning/03_first-order-logic/02_quantifiers.tex} +\input{parts/02_formal-reasoning/04_equality.tex} +\input{parts/02_formal-reasoning/05_correctness/00_intro.tex} +\input{parts/02_formal-reasoning/05_correctness/01_termination.tex} +\input{parts/02_formal-reasoning/05_correctness/02_behaviour.tex} +% \input{parts/02_formal-reasoning/05_correctness/} +% \input{parts/02_formal-reasoning/} \newsection \section{Typing} -\input{parts/02_typing/00_intro.tex} -\input{parts/02_typing/01_mini-haskell/00_syntax.tex} -\input{parts/02_typing/01_mini-haskell/01_lambda-calculus.tex} -\input{parts/02_typing/01_mini-haskell/02_further-rules.tex} -\input{parts/02_typing/01_mini-haskell/03_type-inference.tex} -\input{parts/02_typing/02_algebraic-data-types/00_correctness.tex} -\input{parts/02_typing/02_algebraic-data-types/01_induction-nat-num.tex} -\input{parts/02_typing/02_algebraic-data-types/02_lists.tex} -\input{parts/02_typing/02_algebraic-data-types/03_trees.tex} -\input{parts/02_typing/02_algebraic-data-types/04_structural-induction.tex} -\input{parts/02_typing/03_interpreter/00_intro.tex} -\input{parts/02_typing/03_interpreter/01_read.tex} -\input{parts/02_typing/03_interpreter/02_eval.tex} -% \input{parts/02_typing/03_interpreter/} +\input{parts/03_typing/00_intro.tex} +\input{parts/03_typing/01_mini-haskell/00_syntax.tex} +\input{parts/03_typing/01_mini-haskell/01_lambda-calculus.tex} +\input{parts/03_typing/01_mini-haskell/02_further-rules.tex} +\input{parts/03_typing/01_mini-haskell/03_type-inference.tex} +\input{parts/03_typing/02_algebraic-data-types/00_correctness.tex} +\input{parts/03_typing/02_algebraic-data-types/01_induction-nat-num.tex} +\input{parts/03_typing/02_algebraic-data-types/02_lists.tex} +\input{parts/03_typing/02_algebraic-data-types/03_trees.tex} +\input{parts/03_typing/03_interpreter/00_intro.tex} +\input{parts/03_typing/03_interpreter/01_read.tex} +\input{parts/03_typing/03_interpreter/02_eval.tex} +% \input{parts/03_typing/03_interpreter/} \newsection \section{Language Semantics} -\input{parts/03_language-semantics/00_imp/00_syntax.tex} -\input{parts/03_language-semantics/00_imp/01_semantics.tex} -\input{parts/03_language-semantics/00_imp/02_properties.tex} -\input{parts/03_language-semantics/01_operational-semantics/00_big-step-semantics/00_transition-systems.tex} -\input{parts/03_language-semantics/01_operational-semantics/00_big-step-semantics/01_semantics.tex} -\input{parts/03_language-semantics/01_operational-semantics/00_big-step-semantics/02_instantiations.tex} -\input{parts/03_language-semantics/01_operational-semantics/00_big-step-semantics/03_termination.tex} -\input{parts/03_language-semantics/01_operational-semantics/00_big-step-semantics/04_semantic-equivalence.tex} -\input{parts/03_language-semantics/01_operational-semantics/00_big-step-semantics/05_unfolding-loops.tex} -\input{parts/03_language-semantics/01_operational-semantics/00_big-step-semantics/06_deterministic-semantics.tex} -\input{parts/03_language-semantics/01_operational-semantics/00_big-step-semantics/07_extensions-of-imp.tex} -\input{parts/03_language-semantics/01_operational-semantics/01_small-step-semantics/00_structural-operational-semantics.tex} -\input{parts/03_language-semantics/01_operational-semantics/01_small-step-semantics/01_rules.tex} -\input{parts/03_language-semantics/01_operational-semantics/01_small-step-semantics/02_multi-step-derivation-seq.tex} -\input{parts/03_language-semantics/01_operational-semantics/01_small-step-semantics/03_termintation.tex} -\input{parts/03_language-semantics/01_operational-semantics/01_small-step-semantics/04_proofs.tex} -\input{parts/03_language-semantics/01_operational-semantics/01_small-step-semantics/05_semantic-equivalence.tex} -\input{parts/03_language-semantics/01_operational-semantics/01_small-step-semantics/06_extensions.tex} -\input{parts/03_language-semantics/01_operational-semantics/02_equiv.tex} -\input{parts/03_language-semantics/01_operational-semantics/03_rules-summary.tex} -\input{parts/03_language-semantics/02_axiomatic-semantics/00_intro.tex} -\input{parts/03_language-semantics/02_axiomatic-semantics/01_hoare-logic/00_triples-assertions.tex} -\input{parts/03_language-semantics/02_axiomatic-semantics/01_hoare-logic/01_derivation-systems.tex} -\input{parts/03_language-semantics/02_axiomatic-semantics/01_hoare-logic/02_total-correctness.tex} -\input{parts/03_language-semantics/02_axiomatic-semantics/02_soundness-completeness.tex} -% \input{parts/03_language-semantics/} +\input{parts/04_language-semantics/00_imp/00_syntax.tex} +\input{parts/04_language-semantics/00_imp/01_semantics.tex} +\input{parts/04_language-semantics/00_imp/02_properties.tex} +\input{parts/04_language-semantics/01_operational-semantics/00_big-step-semantics/00_transition-systems.tex} +\input{parts/04_language-semantics/01_operational-semantics/00_big-step-semantics/01_semantics.tex} +\input{parts/04_language-semantics/01_operational-semantics/00_big-step-semantics/02_instantiations.tex} +\input{parts/04_language-semantics/01_operational-semantics/00_big-step-semantics/03_termination.tex} +\input{parts/04_language-semantics/01_operational-semantics/00_big-step-semantics/04_semantic-equivalence.tex} +\input{parts/04_language-semantics/01_operational-semantics/00_big-step-semantics/05_unfolding-loops.tex} +\input{parts/04_language-semantics/01_operational-semantics/00_big-step-semantics/06_deterministic-semantics.tex} +\input{parts/04_language-semantics/01_operational-semantics/00_big-step-semantics/07_extensions-of-imp.tex} +\input{parts/04_language-semantics/01_operational-semantics/01_small-step-semantics/00_structural-operational-semantics.tex} +\input{parts/04_language-semantics/01_operational-semantics/01_small-step-semantics/01_rules.tex} +\input{parts/04_language-semantics/01_operational-semantics/01_small-step-semantics/02_multi-step-derivation-seq.tex} +\input{parts/04_language-semantics/01_operational-semantics/01_small-step-semantics/03_termintation.tex} +\input{parts/04_language-semantics/01_operational-semantics/01_small-step-semantics/04_proofs.tex} +\input{parts/04_language-semantics/01_operational-semantics/01_small-step-semantics/05_semantic-equivalence.tex} +\input{parts/04_language-semantics/01_operational-semantics/01_small-step-semantics/06_extensions.tex} +\input{parts/04_language-semantics/01_operational-semantics/02_equiv.tex} +\input{parts/04_language-semantics/01_operational-semantics/03_rules-summary.tex} +\input{parts/04_language-semantics/02_axiomatic-semantics/00_intro.tex} +\input{parts/04_language-semantics/02_axiomatic-semantics/01_hoare-logic/00_triples-assertions.tex} +\input{parts/04_language-semantics/02_axiomatic-semantics/01_hoare-logic/01_derivation-systems.tex} +\input{parts/04_language-semantics/02_axiomatic-semantics/01_hoare-logic/02_total-correctness.tex} +\input{parts/04_language-semantics/02_axiomatic-semantics/02_soundness-completeness.tex} +% \input{parts/04_language-semantics/} \newsection \section{Modelling} -\input{parts/04_modelling/00_intro.tex} -\input{parts/04_modelling/01_promela/00_syntax.tex} -\input{parts/04_modelling/01_promela/01_expressions.tex} -\input{parts/04_modelling/01_promela/02_statements.tex} -\input{parts/04_modelling/01_promela/03_macros.tex} -\input{parts/04_modelling/02_linear-temporal-logic/00_linear-time-properties.tex} -\input{parts/04_modelling/02_linear-temporal-logic/01_linear-temporal-logic.tex} -% \input{parts/04_modelling/02_linear-temporal-logic/} -% \input{parts/04_modelling/} +\input{parts/05_modelling/00_intro.tex} +\input{parts/05_modelling/01_promela/00_syntax.tex} +\input{parts/05_modelling/01_promela/01_expressions.tex} +\input{parts/05_modelling/01_promela/02_statements.tex} +\input{parts/05_modelling/01_promela/03_macros.tex} +\input{parts/05_modelling/02_linear-temporal-logic/00_linear-time-properties.tex} +\input{parts/05_modelling/02_linear-temporal-logic/01_linear-temporal-logic.tex} +% \input{parts/05_modelling/02_linear-temporal-logic/} +% \input{parts/05_modelling/} diff --git a/semester4/fmfp/parts/01_formal-reasoning/05_correctness/03_induction.tex b/semester4/fmfp/parts/01_formal-reasoning/05_correctness/03_induction.tex deleted file mode 100644 index f6b79dd..0000000 --- a/semester4/fmfp/parts/01_formal-reasoning/05_correctness/03_induction.tex +++ /dev/null @@ -1,25 +0,0 @@ -\subsubsection{Induction} -To prove recursive formulas, or more precisely formulated, a formula $P$ (with free variable $n$) for all $n \in \N$, -we can't really do a proof by cases, as there are infinitely many cases (one for each input). -Thus: We can use induction to prove recursive formulas or functions. - - -\paragraph{The schema} -To prove $\forall n \in \N. P$ (with $n$ free in $P$), we do the following: - -\shade{blue}{Base case} We show that $P[n \mapsto 0]$ is correct - -\shade{green}{Step case} For an arbitrary $m$ not free in $P$, we show that $P[n \mapsto m + 1]$ is correct under the assumption that $P[n \mapsto m]$ is correct. - -For \bi{well-founded} domains, we have to adjust the induction hypothesis slightly: We assume $\forall l \in \N. l < m \rightarrow P[n \mapsto l]$ -and then prove $P[n \mapsto m]$ under our assumption. - - -\paragraph{Induction over Lists} -To prove $P$ for all $xs$ in \texttt{[T]}, we do the following: - -\shade{blue}{Base case} We prove that $P[xs \mapsto []]$ is correct - -\shade{green}{Step case} We prove that $\forall y :: T, ys :: [T]. P[xs \mapsto ys] \rightarrow P[xs \mapsto y : ys]$, or in other words: -We fix arbitrary $y :: T$ and $ys :: [T]$, which both are not free in $P$. -We then apply our induction hypothesis $P[xs \mapsto ys]$ to prove $P[xs \mapsto y : ys]$ diff --git a/semester4/fmfp/parts/01_induction-proofs/00_intro.tex b/semester4/fmfp/parts/01_induction-proofs/00_intro.tex new file mode 100644 index 0000000..77d6a74 --- /dev/null +++ b/semester4/fmfp/parts/01_induction-proofs/00_intro.tex @@ -0,0 +1,6 @@ +To prove recursive formulas, or more precisely formulated, a formula $P$ (with free variable $n$) for all $n \in \N$, +we have can use weak or strong induction. +Weak induction may be a \textit{slightly} misleading term, because it isn't necessarily weaker than strong induction. + +This section has been moved to the very start of the theory part, even though many of the topics mentioned have not been covered in the summary yet, +such that all the induction proofs can be covered in the same place. diff --git a/semester4/fmfp/parts/01_induction-proofs/01_mathematical-induction.tex b/semester4/fmfp/parts/01_induction-proofs/01_mathematical-induction.tex new file mode 100644 index 0000000..c8bc8be --- /dev/null +++ b/semester4/fmfp/parts/01_induction-proofs/01_mathematical-induction.tex @@ -0,0 +1,24 @@ +\subsection{Mathematical Induction} +{\small NOTE: These types of induction were (primarily) mentioned in the Formal Methods part of the course, but made most sense to be put here} + +\subsubsection{Weak Mathematical Induction} +To prove $\forall n \in \N. P$ (with $n$ free in $P$), we do the following: + +\shade{blue}{Base case} We show that $P[n \mapsto 0]$ is correct + +\shade{green}{Step case} For an arbitrary $m$ not free in $P$, we show that $P[n \mapsto m + 1]$ is correct under the assumption that $P[n \mapsto m]$ is correct. + +For \bi{well-founded} domains, we have to adjust the induction hypothesis slightly: We assume $\forall l \in \N. l < m \rightarrow P[n \mapsto l]$ +and then prove $P[n \mapsto m]$ under our assumption. + +The same, but expressed as a Natural Deduction rule: +\[ + \begin{prooftree} + \hypo{\Gamma \vdash P(0)} + \hypo{\Gamma, P(n) \vdash P(n + 1)} + \infer2{\Gamma \vdash \forall n. P(n)} + \end{prooftree} +\] + + +\subsubsection{Strong Mathematical Induction} diff --git a/semester4/fmfp/parts/02_typing/02_algebraic-data-types/04_structural-induction.tex b/semester4/fmfp/parts/01_induction-proofs/02_structural-induction.tex similarity index 91% rename from semester4/fmfp/parts/02_typing/02_algebraic-data-types/04_structural-induction.tex rename to semester4/fmfp/parts/01_induction-proofs/02_structural-induction.tex index cc1bd6f..1edbc48 100644 --- a/semester4/fmfp/parts/02_typing/02_algebraic-data-types/04_structural-induction.tex +++ b/semester4/fmfp/parts/01_induction-proofs/02_structural-induction.tex @@ -1,4 +1,5 @@ -\subsubsection{Structural Induction} +\subsection{Structural Induction} +\subsubsection{Weak Structural Induction} Induction is based on the structure of terms \mint{haskell}+data T t = Leaf t | Node1 (T t) | Node2 t (T t) (T t)+ diff --git a/semester4/fmfp/parts/01_induction-proofs/03_induction-on-trees.tex b/semester4/fmfp/parts/01_induction-proofs/03_induction-on-trees.tex new file mode 100644 index 0000000..e69de29 diff --git a/semester4/fmfp/parts/01_induction-proofs/04_other-induction.tex b/semester4/fmfp/parts/01_induction-proofs/04_other-induction.tex new file mode 100644 index 0000000..7ca3fec --- /dev/null +++ b/semester4/fmfp/parts/01_induction-proofs/04_other-induction.tex @@ -0,0 +1,11 @@ +\subsection{Other types of induction} +\subsubsection{Induction over Lists} +To prove $P$ for all $xs$ in \texttt{[T]}, we do the following: + +\shade{blue}{Base case} We prove that $P[xs \mapsto []]$ is correct + +\shade{green}{Step case} We prove that $\forall y :: T, ys :: [T]. P[xs \mapsto ys] \rightarrow P[xs \mapsto y : ys]$, or in other words: +We fix arbitrary $y :: T$ and $ys :: [T]$, which both are not free in $P$. +We then apply our induction hypothesis $P[xs \mapsto ys]$ to prove $P[xs \mapsto y : ys]$ + + diff --git a/semester4/fmfp/parts/01_formal-reasoning/00_formal-proofs.tex b/semester4/fmfp/parts/02_formal-reasoning/00_formal-proofs.tex similarity index 100% rename from semester4/fmfp/parts/01_formal-reasoning/00_formal-proofs.tex rename to semester4/fmfp/parts/02_formal-reasoning/00_formal-proofs.tex diff --git a/semester4/fmfp/parts/01_formal-reasoning/01_natural-deduction.tex b/semester4/fmfp/parts/02_formal-reasoning/01_natural-deduction.tex similarity index 100% rename from semester4/fmfp/parts/01_formal-reasoning/01_natural-deduction.tex rename to semester4/fmfp/parts/02_formal-reasoning/01_natural-deduction.tex diff --git a/semester4/fmfp/parts/01_formal-reasoning/02_propositional-logic/00_syntax.tex b/semester4/fmfp/parts/02_formal-reasoning/02_propositional-logic/00_syntax.tex similarity index 100% rename from semester4/fmfp/parts/01_formal-reasoning/02_propositional-logic/00_syntax.tex rename to semester4/fmfp/parts/02_formal-reasoning/02_propositional-logic/00_syntax.tex diff --git a/semester4/fmfp/parts/01_formal-reasoning/02_propositional-logic/01_semantics.tex b/semester4/fmfp/parts/02_formal-reasoning/02_propositional-logic/01_semantics.tex similarity index 100% rename from semester4/fmfp/parts/01_formal-reasoning/02_propositional-logic/01_semantics.tex rename to semester4/fmfp/parts/02_formal-reasoning/02_propositional-logic/01_semantics.tex diff --git a/semester4/fmfp/parts/01_formal-reasoning/02_propositional-logic/02_deductive-system.tex b/semester4/fmfp/parts/02_formal-reasoning/02_propositional-logic/02_deductive-system.tex similarity index 100% rename from semester4/fmfp/parts/01_formal-reasoning/02_propositional-logic/02_deductive-system.tex rename to semester4/fmfp/parts/02_formal-reasoning/02_propositional-logic/02_deductive-system.tex diff --git a/semester4/fmfp/parts/01_formal-reasoning/02_propositional-logic/03_natural-deduction-prop-logic.tex b/semester4/fmfp/parts/02_formal-reasoning/02_propositional-logic/03_natural-deduction-prop-logic.tex similarity index 100% rename from semester4/fmfp/parts/01_formal-reasoning/02_propositional-logic/03_natural-deduction-prop-logic.tex rename to semester4/fmfp/parts/02_formal-reasoning/02_propositional-logic/03_natural-deduction-prop-logic.tex diff --git a/semester4/fmfp/parts/01_formal-reasoning/02_propositional-logic/04_derivation-rules-overview.tex b/semester4/fmfp/parts/02_formal-reasoning/02_propositional-logic/04_derivation-rules-overview.tex similarity index 100% rename from semester4/fmfp/parts/01_formal-reasoning/02_propositional-logic/04_derivation-rules-overview.tex rename to semester4/fmfp/parts/02_formal-reasoning/02_propositional-logic/04_derivation-rules-overview.tex diff --git a/semester4/fmfp/parts/01_formal-reasoning/03_first-order-logic/00_syntax.tex b/semester4/fmfp/parts/02_formal-reasoning/03_first-order-logic/00_syntax.tex similarity index 100% rename from semester4/fmfp/parts/01_formal-reasoning/03_first-order-logic/00_syntax.tex rename to semester4/fmfp/parts/02_formal-reasoning/03_first-order-logic/00_syntax.tex diff --git a/semester4/fmfp/parts/01_formal-reasoning/03_first-order-logic/01_semantics.tex b/semester4/fmfp/parts/02_formal-reasoning/03_first-order-logic/01_semantics.tex similarity index 100% rename from semester4/fmfp/parts/01_formal-reasoning/03_first-order-logic/01_semantics.tex rename to semester4/fmfp/parts/02_formal-reasoning/03_first-order-logic/01_semantics.tex diff --git a/semester4/fmfp/parts/01_formal-reasoning/03_first-order-logic/02_quantifiers.tex b/semester4/fmfp/parts/02_formal-reasoning/03_first-order-logic/02_quantifiers.tex similarity index 100% rename from semester4/fmfp/parts/01_formal-reasoning/03_first-order-logic/02_quantifiers.tex rename to semester4/fmfp/parts/02_formal-reasoning/03_first-order-logic/02_quantifiers.tex diff --git a/semester4/fmfp/parts/01_formal-reasoning/04_equality.tex b/semester4/fmfp/parts/02_formal-reasoning/04_equality.tex similarity index 100% rename from semester4/fmfp/parts/01_formal-reasoning/04_equality.tex rename to semester4/fmfp/parts/02_formal-reasoning/04_equality.tex diff --git a/semester4/fmfp/parts/01_formal-reasoning/05_correctness/00_intro.tex b/semester4/fmfp/parts/02_formal-reasoning/05_correctness/00_intro.tex similarity index 100% rename from semester4/fmfp/parts/01_formal-reasoning/05_correctness/00_intro.tex rename to semester4/fmfp/parts/02_formal-reasoning/05_correctness/00_intro.tex diff --git a/semester4/fmfp/parts/01_formal-reasoning/05_correctness/01_termination.tex b/semester4/fmfp/parts/02_formal-reasoning/05_correctness/01_termination.tex similarity index 100% rename from semester4/fmfp/parts/01_formal-reasoning/05_correctness/01_termination.tex rename to semester4/fmfp/parts/02_formal-reasoning/05_correctness/01_termination.tex diff --git a/semester4/fmfp/parts/01_formal-reasoning/05_correctness/02_behaviour.tex b/semester4/fmfp/parts/02_formal-reasoning/05_correctness/02_behaviour.tex similarity index 91% rename from semester4/fmfp/parts/01_formal-reasoning/05_correctness/02_behaviour.tex rename to semester4/fmfp/parts/02_formal-reasoning/05_correctness/02_behaviour.tex index 53561f7..57a6d71 100644 --- a/semester4/fmfp/parts/01_formal-reasoning/05_correctness/02_behaviour.tex +++ b/semester4/fmfp/parts/02_formal-reasoning/05_correctness/02_behaviour.tex @@ -41,4 +41,4 @@ We then show that the function is correct for both cases (i.e. LHS and RHS of OR \end{enumerate} In this proof we used the \textbf{TND} and \textbf{$\lor$-E} (here also called \bi{Case Split}) rules. -So what we have to show, given $Q \lor R$ for any proposition $P$ with case split is that \bi{(1)} $P$ follows from $Q$ and \bi{(2)} $P$ follows from $R$ +What we have to show, given $Q \lor R$ for any proposition $P$ with case split, is that \bi{(1)} $P$ follows from $Q$ and \bi{(2)} $P$ follows from $R$ diff --git a/semester4/fmfp/parts/02_typing/00_intro.tex b/semester4/fmfp/parts/03_typing/00_intro.tex similarity index 100% rename from semester4/fmfp/parts/02_typing/00_intro.tex rename to semester4/fmfp/parts/03_typing/00_intro.tex diff --git a/semester4/fmfp/parts/02_typing/01_mini-haskell/00_syntax.tex b/semester4/fmfp/parts/03_typing/01_mini-haskell/00_syntax.tex similarity index 100% rename from semester4/fmfp/parts/02_typing/01_mini-haskell/00_syntax.tex rename to semester4/fmfp/parts/03_typing/01_mini-haskell/00_syntax.tex diff --git a/semester4/fmfp/parts/02_typing/01_mini-haskell/01_lambda-calculus.tex b/semester4/fmfp/parts/03_typing/01_mini-haskell/01_lambda-calculus.tex similarity index 100% rename from semester4/fmfp/parts/02_typing/01_mini-haskell/01_lambda-calculus.tex rename to semester4/fmfp/parts/03_typing/01_mini-haskell/01_lambda-calculus.tex diff --git a/semester4/fmfp/parts/02_typing/01_mini-haskell/02_further-rules.tex b/semester4/fmfp/parts/03_typing/01_mini-haskell/02_further-rules.tex similarity index 100% rename from semester4/fmfp/parts/02_typing/01_mini-haskell/02_further-rules.tex rename to semester4/fmfp/parts/03_typing/01_mini-haskell/02_further-rules.tex diff --git a/semester4/fmfp/parts/02_typing/01_mini-haskell/03_type-inference.tex b/semester4/fmfp/parts/03_typing/01_mini-haskell/03_type-inference.tex similarity index 100% rename from semester4/fmfp/parts/02_typing/01_mini-haskell/03_type-inference.tex rename to semester4/fmfp/parts/03_typing/01_mini-haskell/03_type-inference.tex diff --git a/semester4/fmfp/parts/02_typing/02_algebraic-data-types/00_correctness.tex b/semester4/fmfp/parts/03_typing/02_algebraic-data-types/00_correctness.tex similarity index 100% rename from semester4/fmfp/parts/02_typing/02_algebraic-data-types/00_correctness.tex rename to semester4/fmfp/parts/03_typing/02_algebraic-data-types/00_correctness.tex diff --git a/semester4/fmfp/parts/02_typing/02_algebraic-data-types/01_induction-nat-num.tex b/semester4/fmfp/parts/03_typing/02_algebraic-data-types/01_induction-nat-num.tex similarity index 100% rename from semester4/fmfp/parts/02_typing/02_algebraic-data-types/01_induction-nat-num.tex rename to semester4/fmfp/parts/03_typing/02_algebraic-data-types/01_induction-nat-num.tex diff --git a/semester4/fmfp/parts/02_typing/02_algebraic-data-types/02_lists.tex b/semester4/fmfp/parts/03_typing/02_algebraic-data-types/02_lists.tex similarity index 100% rename from semester4/fmfp/parts/02_typing/02_algebraic-data-types/02_lists.tex rename to semester4/fmfp/parts/03_typing/02_algebraic-data-types/02_lists.tex diff --git a/semester4/fmfp/parts/02_typing/02_algebraic-data-types/03_trees.tex b/semester4/fmfp/parts/03_typing/02_algebraic-data-types/03_trees.tex similarity index 100% rename from semester4/fmfp/parts/02_typing/02_algebraic-data-types/03_trees.tex rename to semester4/fmfp/parts/03_typing/02_algebraic-data-types/03_trees.tex diff --git a/semester4/fmfp/parts/02_typing/03_interpreter/00_intro.tex b/semester4/fmfp/parts/03_typing/03_interpreter/00_intro.tex similarity index 100% rename from semester4/fmfp/parts/02_typing/03_interpreter/00_intro.tex rename to semester4/fmfp/parts/03_typing/03_interpreter/00_intro.tex diff --git a/semester4/fmfp/parts/02_typing/03_interpreter/01_read.tex b/semester4/fmfp/parts/03_typing/03_interpreter/01_read.tex similarity index 100% rename from semester4/fmfp/parts/02_typing/03_interpreter/01_read.tex rename to semester4/fmfp/parts/03_typing/03_interpreter/01_read.tex diff --git a/semester4/fmfp/parts/02_typing/03_interpreter/02_eval.tex b/semester4/fmfp/parts/03_typing/03_interpreter/02_eval.tex similarity index 100% rename from semester4/fmfp/parts/02_typing/03_interpreter/02_eval.tex rename to semester4/fmfp/parts/03_typing/03_interpreter/02_eval.tex diff --git a/semester4/fmfp/parts/03_language-semantics/00_imp/00_syntax.tex b/semester4/fmfp/parts/04_language-semantics/00_imp/00_syntax.tex similarity index 100% rename from semester4/fmfp/parts/03_language-semantics/00_imp/00_syntax.tex rename to semester4/fmfp/parts/04_language-semantics/00_imp/00_syntax.tex diff --git a/semester4/fmfp/parts/03_language-semantics/00_imp/01_semantics.tex b/semester4/fmfp/parts/04_language-semantics/00_imp/01_semantics.tex similarity index 97% rename from semester4/fmfp/parts/03_language-semantics/00_imp/01_semantics.tex rename to semester4/fmfp/parts/04_language-semantics/00_imp/01_semantics.tex index 4bd2938..0b56e7f 100644 --- a/semester4/fmfp/parts/03_language-semantics/00_imp/01_semantics.tex +++ b/semester4/fmfp/parts/04_language-semantics/00_imp/01_semantics.tex @@ -1,3 +1,4 @@ +\newpage \subsubsection{The semantics} \paragraph{Numerals} The semantic function $\cN : \texttt{Numeral} \rightarrow \texttt{Val}$ maps a numeral $n$ to an integer value $\cN\llbracket n \rrbracket$, @@ -27,7 +28,7 @@ $\cA : \texttt{Aexp} \rightarrow \texttt{State} \rightarrow \texttt{Val}$ maps a given by: \begin{align*} \cA\llbracket x \rrbracket \sigma & = \sigma(x) \\ - \cA\llbracket n \rrbracket \sigma & = \cN\llbracket x \rrbracket \\ + \cA\llbracket n \rrbracket \sigma & = \cN\llbracket n \rrbracket \\ \cA\llbracket e_1 \; \texttt{op} \; e_2 \rrbracket \sigma & = \cA\llbracket e_1 \rrbracket \sigma \; \overline{\texttt{op}} \; \cA\llbracket e_2 \rrbracket \sigma \end{align*} For $\texttt{op} \in \texttt{Op}$, $\overline{\texttt{op}}$ is the corresponding operation $\texttt{Val} \times \texttt{Val} \rightarrow \texttt{Val}$ diff --git a/semester4/fmfp/parts/03_language-semantics/00_imp/02_properties.tex b/semester4/fmfp/parts/04_language-semantics/00_imp/02_properties.tex similarity index 95% rename from semester4/fmfp/parts/03_language-semantics/00_imp/02_properties.tex rename to semester4/fmfp/parts/04_language-semantics/00_imp/02_properties.tex index cf1f2f2..0e71782 100644 --- a/semester4/fmfp/parts/03_language-semantics/00_imp/02_properties.tex +++ b/semester4/fmfp/parts/04_language-semantics/00_imp/02_properties.tex @@ -24,7 +24,6 @@ If on the other hand we define $\cA\llbracket -e \rrbracket \sigma = \cA\llbrack it is \textit{not} an inductive definition because $0 - e$ is \textit{not} a subterm of $-e$ -\newpage \paragraph{Free Variables} For Arithmetic Expressions \begin{align*} @@ -36,7 +35,7 @@ For Arithmetic Expressions For Boolean Expressions \begin{align*} FV(b_1 \; \texttt{op} \; b_2) & = FV(b_1) \cup FV(b_2) \\ - FV(\texttt{not} b) & = FV(b) \\ + FV(\texttt{not}\; b) & = FV(b) \\ FV(b_1 \; \texttt{or} \; b_2) & = FV(b_1) \cup FV(b_2) \\ FV(b_1 \; \texttt{and} \; b_2) & = FV(b_1) \cup FV(b_2) \end{align*} @@ -56,7 +55,7 @@ And finally for Statements: A substitution $f[x \mapsto e]$ replaces each free occurrence of variable $x$ in $f$ by $e$, where $f$ is any expression. -Detailed rules for arithmetic expressions: +Detailed rules for arithmetic expressions (for the last, if variable $y$ is $x$, it is replaced, otherwise not): \begin{align*} (e_1 \; \texttt{op} \; e_2)[x \mapsto e] & \equiv (e_1[x \mapsto e] \; \texttt{op} \; e_2[x \mapsto e]) \\ n[x \mapsto e] & \equiv n \\ diff --git a/semester4/fmfp/parts/03_language-semantics/01_operational-semantics/00_big-step-semantics/00_transition-systems.tex b/semester4/fmfp/parts/04_language-semantics/01_operational-semantics/00_big-step-semantics/00_transition-systems.tex similarity index 81% rename from semester4/fmfp/parts/03_language-semantics/01_operational-semantics/00_big-step-semantics/00_transition-systems.tex rename to semester4/fmfp/parts/04_language-semantics/01_operational-semantics/00_big-step-semantics/00_transition-systems.tex index d2f2939..e1f2dbb 100644 --- a/semester4/fmfp/parts/03_language-semantics/01_operational-semantics/00_big-step-semantics/00_transition-systems.tex +++ b/semester4/fmfp/parts/04_language-semantics/01_operational-semantics/00_big-step-semantics/00_transition-systems.tex @@ -1,7 +1,7 @@ \newpage \subsection{Operational Semantics} -Big-step semantics describe how the \bi{overall} results of the execution are obtained and use Natural semantics rules. -Small-step semantics describe how the individual steps of the computations take place and use Structural Operational Semantics (SOS) +\textbf{Big-step semantics} describe how the \bi{overall} results of the execution are obtained and use Natural semantics rules. +\textbf{Small-step semantics} describe how the individual steps of the computations take place and use Structural Operational Semantics (SOS) \subsubsection{Big-Step Semantics} \paragraph{Transition Systems} diff --git a/semester4/fmfp/parts/03_language-semantics/01_operational-semantics/00_big-step-semantics/01_semantics.tex b/semester4/fmfp/parts/04_language-semantics/01_operational-semantics/00_big-step-semantics/01_semantics.tex similarity index 100% rename from semester4/fmfp/parts/03_language-semantics/01_operational-semantics/00_big-step-semantics/01_semantics.tex rename to semester4/fmfp/parts/04_language-semantics/01_operational-semantics/00_big-step-semantics/01_semantics.tex diff --git a/semester4/fmfp/parts/03_language-semantics/01_operational-semantics/00_big-step-semantics/02_instantiations.tex b/semester4/fmfp/parts/04_language-semantics/01_operational-semantics/00_big-step-semantics/02_instantiations.tex similarity index 92% rename from semester4/fmfp/parts/03_language-semantics/01_operational-semantics/00_big-step-semantics/02_instantiations.tex rename to semester4/fmfp/parts/04_language-semantics/01_operational-semantics/00_big-step-semantics/02_instantiations.tex index 5b6968d..8f42c69 100644 --- a/semester4/fmfp/parts/03_language-semantics/01_operational-semantics/00_big-step-semantics/02_instantiations.tex +++ b/semester4/fmfp/parts/04_language-semantics/01_operational-semantics/00_big-step-semantics/02_instantiations.tex @@ -2,8 +2,8 @@ Each inference rule is actually a rule scheme, where the meta-variables are placeholders for statements, states, etc. Each rule scheme describes infinitely many \bi{rule instances}. -A rule is \bi{instantiated} when all meta-variables are replaced with syntactic elements -Assignment rule scheme vs. instance +A rule is \bi{instantiated} when all meta-variables are replaced with syntactic elements. +Assignment rule scheme vs. instance: \[ \begin{prooftree} \infer0[\textsc{Ass}$_{NS}$]{\langle x := e, \sigma \rangle \rightarrow \sigma[x \mapsto \cA\llbracket e \rrbracket \sigma]} diff --git a/semester4/fmfp/parts/03_language-semantics/01_operational-semantics/00_big-step-semantics/03_termination.tex b/semester4/fmfp/parts/04_language-semantics/01_operational-semantics/00_big-step-semantics/03_termination.tex similarity index 100% rename from semester4/fmfp/parts/03_language-semantics/01_operational-semantics/00_big-step-semantics/03_termination.tex rename to semester4/fmfp/parts/04_language-semantics/01_operational-semantics/00_big-step-semantics/03_termination.tex diff --git a/semester4/fmfp/parts/03_language-semantics/01_operational-semantics/00_big-step-semantics/04_semantic-equivalence.tex b/semester4/fmfp/parts/04_language-semantics/01_operational-semantics/00_big-step-semantics/04_semantic-equivalence.tex similarity index 100% rename from semester4/fmfp/parts/03_language-semantics/01_operational-semantics/00_big-step-semantics/04_semantic-equivalence.tex rename to semester4/fmfp/parts/04_language-semantics/01_operational-semantics/00_big-step-semantics/04_semantic-equivalence.tex diff --git a/semester4/fmfp/parts/03_language-semantics/01_operational-semantics/00_big-step-semantics/05_unfolding-loops.tex b/semester4/fmfp/parts/04_language-semantics/01_operational-semantics/00_big-step-semantics/05_unfolding-loops.tex similarity index 100% rename from semester4/fmfp/parts/03_language-semantics/01_operational-semantics/00_big-step-semantics/05_unfolding-loops.tex rename to semester4/fmfp/parts/04_language-semantics/01_operational-semantics/00_big-step-semantics/05_unfolding-loops.tex diff --git a/semester4/fmfp/parts/03_language-semantics/01_operational-semantics/00_big-step-semantics/06_deterministic-semantics.tex b/semester4/fmfp/parts/04_language-semantics/01_operational-semantics/00_big-step-semantics/06_deterministic-semantics.tex similarity index 100% rename from semester4/fmfp/parts/03_language-semantics/01_operational-semantics/00_big-step-semantics/06_deterministic-semantics.tex rename to semester4/fmfp/parts/04_language-semantics/01_operational-semantics/00_big-step-semantics/06_deterministic-semantics.tex diff --git a/semester4/fmfp/parts/03_language-semantics/01_operational-semantics/00_big-step-semantics/07_extensions-of-imp.tex b/semester4/fmfp/parts/04_language-semantics/01_operational-semantics/00_big-step-semantics/07_extensions-of-imp.tex similarity index 100% rename from semester4/fmfp/parts/03_language-semantics/01_operational-semantics/00_big-step-semantics/07_extensions-of-imp.tex rename to semester4/fmfp/parts/04_language-semantics/01_operational-semantics/00_big-step-semantics/07_extensions-of-imp.tex diff --git a/semester4/fmfp/parts/03_language-semantics/01_operational-semantics/01_small-step-semantics/00_structural-operational-semantics.tex b/semester4/fmfp/parts/04_language-semantics/01_operational-semantics/01_small-step-semantics/00_structural-operational-semantics.tex similarity index 100% rename from semester4/fmfp/parts/03_language-semantics/01_operational-semantics/01_small-step-semantics/00_structural-operational-semantics.tex rename to semester4/fmfp/parts/04_language-semantics/01_operational-semantics/01_small-step-semantics/00_structural-operational-semantics.tex diff --git a/semester4/fmfp/parts/03_language-semantics/01_operational-semantics/01_small-step-semantics/01_rules.tex b/semester4/fmfp/parts/04_language-semantics/01_operational-semantics/01_small-step-semantics/01_rules.tex similarity index 100% rename from semester4/fmfp/parts/03_language-semantics/01_operational-semantics/01_small-step-semantics/01_rules.tex rename to semester4/fmfp/parts/04_language-semantics/01_operational-semantics/01_small-step-semantics/01_rules.tex diff --git a/semester4/fmfp/parts/03_language-semantics/01_operational-semantics/01_small-step-semantics/02_multi-step-derivation-seq.tex b/semester4/fmfp/parts/04_language-semantics/01_operational-semantics/01_small-step-semantics/02_multi-step-derivation-seq.tex similarity index 100% rename from semester4/fmfp/parts/03_language-semantics/01_operational-semantics/01_small-step-semantics/02_multi-step-derivation-seq.tex rename to semester4/fmfp/parts/04_language-semantics/01_operational-semantics/01_small-step-semantics/02_multi-step-derivation-seq.tex diff --git a/semester4/fmfp/parts/03_language-semantics/01_operational-semantics/01_small-step-semantics/03_termintation.tex b/semester4/fmfp/parts/04_language-semantics/01_operational-semantics/01_small-step-semantics/03_termintation.tex similarity index 100% rename from semester4/fmfp/parts/03_language-semantics/01_operational-semantics/01_small-step-semantics/03_termintation.tex rename to semester4/fmfp/parts/04_language-semantics/01_operational-semantics/01_small-step-semantics/03_termintation.tex diff --git a/semester4/fmfp/parts/03_language-semantics/01_operational-semantics/01_small-step-semantics/04_proofs.tex b/semester4/fmfp/parts/04_language-semantics/01_operational-semantics/01_small-step-semantics/04_proofs.tex similarity index 100% rename from semester4/fmfp/parts/03_language-semantics/01_operational-semantics/01_small-step-semantics/04_proofs.tex rename to semester4/fmfp/parts/04_language-semantics/01_operational-semantics/01_small-step-semantics/04_proofs.tex diff --git a/semester4/fmfp/parts/03_language-semantics/01_operational-semantics/01_small-step-semantics/05_semantic-equivalence.tex b/semester4/fmfp/parts/04_language-semantics/01_operational-semantics/01_small-step-semantics/05_semantic-equivalence.tex similarity index 100% rename from semester4/fmfp/parts/03_language-semantics/01_operational-semantics/01_small-step-semantics/05_semantic-equivalence.tex rename to semester4/fmfp/parts/04_language-semantics/01_operational-semantics/01_small-step-semantics/05_semantic-equivalence.tex diff --git a/semester4/fmfp/parts/03_language-semantics/01_operational-semantics/01_small-step-semantics/06_extensions.tex b/semester4/fmfp/parts/04_language-semantics/01_operational-semantics/01_small-step-semantics/06_extensions.tex similarity index 100% rename from semester4/fmfp/parts/03_language-semantics/01_operational-semantics/01_small-step-semantics/06_extensions.tex rename to semester4/fmfp/parts/04_language-semantics/01_operational-semantics/01_small-step-semantics/06_extensions.tex diff --git a/semester4/fmfp/parts/03_language-semantics/01_operational-semantics/02_equiv.tex b/semester4/fmfp/parts/04_language-semantics/01_operational-semantics/02_equiv.tex similarity index 100% rename from semester4/fmfp/parts/03_language-semantics/01_operational-semantics/02_equiv.tex rename to semester4/fmfp/parts/04_language-semantics/01_operational-semantics/02_equiv.tex diff --git a/semester4/fmfp/parts/03_language-semantics/01_operational-semantics/03_rules-summary.tex b/semester4/fmfp/parts/04_language-semantics/01_operational-semantics/03_rules-summary.tex similarity index 100% rename from semester4/fmfp/parts/03_language-semantics/01_operational-semantics/03_rules-summary.tex rename to semester4/fmfp/parts/04_language-semantics/01_operational-semantics/03_rules-summary.tex diff --git a/semester4/fmfp/parts/03_language-semantics/02_axiomatic-semantics/00_intro.tex b/semester4/fmfp/parts/04_language-semantics/02_axiomatic-semantics/00_intro.tex similarity index 100% rename from semester4/fmfp/parts/03_language-semantics/02_axiomatic-semantics/00_intro.tex rename to semester4/fmfp/parts/04_language-semantics/02_axiomatic-semantics/00_intro.tex diff --git a/semester4/fmfp/parts/03_language-semantics/02_axiomatic-semantics/01_hoare-logic/00_triples-assertions.tex b/semester4/fmfp/parts/04_language-semantics/02_axiomatic-semantics/01_hoare-logic/00_triples-assertions.tex similarity index 100% rename from semester4/fmfp/parts/03_language-semantics/02_axiomatic-semantics/01_hoare-logic/00_triples-assertions.tex rename to semester4/fmfp/parts/04_language-semantics/02_axiomatic-semantics/01_hoare-logic/00_triples-assertions.tex diff --git a/semester4/fmfp/parts/03_language-semantics/02_axiomatic-semantics/01_hoare-logic/01_derivation-systems.tex b/semester4/fmfp/parts/04_language-semantics/02_axiomatic-semantics/01_hoare-logic/01_derivation-systems.tex similarity index 100% rename from semester4/fmfp/parts/03_language-semantics/02_axiomatic-semantics/01_hoare-logic/01_derivation-systems.tex rename to semester4/fmfp/parts/04_language-semantics/02_axiomatic-semantics/01_hoare-logic/01_derivation-systems.tex diff --git a/semester4/fmfp/parts/03_language-semantics/02_axiomatic-semantics/01_hoare-logic/02_total-correctness.tex b/semester4/fmfp/parts/04_language-semantics/02_axiomatic-semantics/01_hoare-logic/02_total-correctness.tex similarity index 100% rename from semester4/fmfp/parts/03_language-semantics/02_axiomatic-semantics/01_hoare-logic/02_total-correctness.tex rename to semester4/fmfp/parts/04_language-semantics/02_axiomatic-semantics/01_hoare-logic/02_total-correctness.tex diff --git a/semester4/fmfp/parts/03_language-semantics/02_axiomatic-semantics/02_soundness-completeness.tex b/semester4/fmfp/parts/04_language-semantics/02_axiomatic-semantics/02_soundness-completeness.tex similarity index 100% rename from semester4/fmfp/parts/03_language-semantics/02_axiomatic-semantics/02_soundness-completeness.tex rename to semester4/fmfp/parts/04_language-semantics/02_axiomatic-semantics/02_soundness-completeness.tex diff --git a/semester4/fmfp/parts/04_modelling/00_intro.tex b/semester4/fmfp/parts/05_modelling/00_intro.tex similarity index 100% rename from semester4/fmfp/parts/04_modelling/00_intro.tex rename to semester4/fmfp/parts/05_modelling/00_intro.tex diff --git a/semester4/fmfp/parts/04_modelling/01_promela/00_syntax.tex b/semester4/fmfp/parts/05_modelling/01_promela/00_syntax.tex similarity index 100% rename from semester4/fmfp/parts/04_modelling/01_promela/00_syntax.tex rename to semester4/fmfp/parts/05_modelling/01_promela/00_syntax.tex diff --git a/semester4/fmfp/parts/04_modelling/01_promela/01_expressions.tex b/semester4/fmfp/parts/05_modelling/01_promela/01_expressions.tex similarity index 100% rename from semester4/fmfp/parts/04_modelling/01_promela/01_expressions.tex rename to semester4/fmfp/parts/05_modelling/01_promela/01_expressions.tex diff --git a/semester4/fmfp/parts/04_modelling/01_promela/02_statements.tex b/semester4/fmfp/parts/05_modelling/01_promela/02_statements.tex similarity index 100% rename from semester4/fmfp/parts/04_modelling/01_promela/02_statements.tex rename to semester4/fmfp/parts/05_modelling/01_promela/02_statements.tex diff --git a/semester4/fmfp/parts/04_modelling/01_promela/03_macros.tex b/semester4/fmfp/parts/05_modelling/01_promela/03_macros.tex similarity index 100% rename from semester4/fmfp/parts/04_modelling/01_promela/03_macros.tex rename to semester4/fmfp/parts/05_modelling/01_promela/03_macros.tex diff --git a/semester4/fmfp/parts/04_modelling/02_linear-temporal-logic/00_linear-time-properties.tex b/semester4/fmfp/parts/05_modelling/02_linear-temporal-logic/00_linear-time-properties.tex similarity index 100% rename from semester4/fmfp/parts/04_modelling/02_linear-temporal-logic/00_linear-time-properties.tex rename to semester4/fmfp/parts/05_modelling/02_linear-temporal-logic/00_linear-time-properties.tex diff --git a/semester4/fmfp/parts/04_modelling/02_linear-temporal-logic/01_linear-temporal-logic.tex b/semester4/fmfp/parts/05_modelling/02_linear-temporal-logic/01_linear-temporal-logic.tex similarity index 100% rename from semester4/fmfp/parts/04_modelling/02_linear-temporal-logic/01_linear-temporal-logic.tex rename to semester4/fmfp/parts/05_modelling/02_linear-temporal-logic/01_linear-temporal-logic.tex