diff options
author | David A. Madore <david+git@madore.org> | 2023-12-04 12:04:26 +0100 |
---|---|---|
committer | David A. Madore <david+git@madore.org> | 2023-12-04 12:04:26 +0100 |
commit | a9e829ce2e76805f228bca36115a4b225d550f98 (patch) | |
tree | e1800ccf534b387af36c47951aecf73adffbeb51 /transp-inf110-02-typage.tex | |
parent | 5dd88ad420e92182d807c7b5ce81eeb37c061d30 (diff) | |
download | inf110-lfi-a9e829ce2e76805f228bca36115a4b225d550f98.tar.gz inf110-lfi-a9e829ce2e76805f228bca36115a4b225d550f98.tar.bz2 inf110-lfi-a9e829ce2e76805f228bca36115a4b225d550f98.zip |
Various minor changes or additions.
Diffstat (limited to 'transp-inf110-02-typage.tex')
-rw-r--r-- | transp-inf110-02-typage.tex | 22 |
1 files changed, 21 insertions, 1 deletions
diff --git a/transp-inf110-02-typage.tex b/transp-inf110-02-typage.tex index 7e4c691..aff8392 100644 --- a/transp-inf110-02-typage.tex +++ b/transp-inf110-02-typage.tex @@ -1828,6 +1828,13 @@ constructivisme russe de A. Markov fils) : resp. $\exists x.P(x)$ passe forcément par la preuve de $P$ ou de $Q$, resp. par la construction d'un $x$ vérifiant $P(x)$. +\bigskip + +\itempoint Les maths « normales » se font en logique classique, mais +certains bouts (explicit\textsuperscript{t} signalés comme tels) de la +littérature sont en logique intuitionniste. On peut y faire de +l'algèbre, de l'analyse, etc., constructives. + \end{frame} % \begin{frame} @@ -2149,7 +2156,7 @@ doute sur la correspondance elle-même. \end{frame} % \begin{frame} -\frametitle{Correspondance de Curry-Howard : exemple avec conjonction} +\frametitle{Correspondance de Curry-Howard : exemple avec disjonction} \itempoint Transformons en programme la démonstration qu'on a donnée de $A\lor B \Rightarrow B\lor A$ @@ -2218,6 +2225,19 @@ $\inferrule*[left={Void}]{\Gamma\vdash r:\bot}{\Gamma\vdash \itempoint Pas de nouvelle règle de réduction à ajouter. +\medskip + +{\footnotesize + +En OCaml : + +{\tt +type void = | ;; +let exfalso = fun (r:void) -> match r with \_ -> . ;; +} + +\par} + \end{frame} % \begin{frame} |