rachel/rachel.cafe
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity

wrote even more on haskell and logic, redo för renskrivning

Browse Source
This commit is contained in:
Rachel Lambda Samuelsson 2022-12-11 19:23:43 +01:00
parent b6f84312e6
commit bb180bc6cb
1 changed files with 37 additions and 10 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

47
_drafts/haskell-and-logic.md
View File

@ -33,6 +33,7 @@ Now given the knowledge that a proposition $P$ is true, we can draw conclusions
* If $P \lor Q$ is true, then we know that at least one of $P$ or $Q$ is true * If $P \lor Q$ is true, then we know that at least one of $P$ or $Q$ is true
* If $P \to Q$ is true, and $P$ is true, then $Q$ is true * If $P \to Q$ is true, and $P$ is true, then $Q$ is true
* If $\lnot P$ is true, then $P$ is false * If $\lnot P$ is true, then $P$ is false
* If $\bot$ is true, then so is everything else (if pigs fly)
There is one more concept I must introduce in order to make proving things interesting, which is that of tautologies and contradictions. A tautology is a statement which is true no matter if the atoms inside of it are true or not, and conversely a contradiction is a statement which is always false. An example of a tautology is $a \to a \lor b$: if $a$ is true then $a \lor b$ is true since $a$ is, if $a$ is false then we need not concern ourself with the motive of the implication. An example of a contradiction is $a \land \lnot a$, this proposition states that $a$ is both true and false, which is impossible. There is one more concept I must introduce in order to make proving things interesting, which is that of tautologies and contradictions. A tautology is a statement which is true no matter if the atoms inside of it are true or not, and conversely a contradiction is a statement which is always false. An example of a tautology is $a \to a \lor b$: if $a$ is true then $a \lor b$ is true since $a$ is, if $a$ is false then we need not concern ourself with the motive of the implication. An example of a contradiction is $a \land \lnot a$, this proposition states that $a$ is both true and false, which is impossible.
@ -109,19 +110,45 @@ proof3 = proof3
``` ```
Well, this is no good, maybe programming languages don't correspond to logic after all? Luckily there is both a solution to this problem. The solution is to "run" our proofs in order to check them, proofs defined this way will either crash or loop forever, so once we see that our proof terminates then we know the proof to be correct. Well, this is no good, maybe programming languages don't correspond to logic after all? Luckily there is both a solution to this problem. The solution is to "run" our proofs in order to check them, proofs defined this way will either crash or loop forever, so once we see that our proof terminates then we know the proof to be correct.
Programming languages studied by logicians usually guarantee termination and don't include values like `undefined` or `error` from Haskell (in fact, the very reason these exist in Haskell is to model non-terminating programs). These programming languages, while they are able to check proofs entirely during typechecking come with their own limitations. Since there is no way to decide if an arbitrary program will terminate ([the halting problem](https://en.wikipedia.org/wiki/Halting_problem)) these programming languages necessarily place restrictions upon what programs are allowed. Consequently these languages are not [Turing-complete](https://en.wikipedia.org/wiki/Turing_completeness), meaning there are programs one cannot write in the language. The programming languages studied by logicians usually guarantee termination and don't include values like `undefined` or `error` from Haskell (in fact, these values, called [bottom](https://wiki.haskell.org/Bottom) exist in Haskell to model non-terminating programs). These programming languages, while they are able to check proofs entirely during typechecking come with their own limitations. Since there is no way to decide if an arbitrary program will terminate ([the halting problem](https://en.wikipedia.org/wiki/Halting_problem)) these programming languages necessarily place restrictions upon what programs are allowed. Consequently these languages are not [Turing-complete](https://en.wikipedia.org/wiki/Turing_completeness), meaning there are programs one cannot write in the language.
## Intuitionism ## Excluding the middle
* Cannot prove all things from logic The logic which we do in Haskell has a name, it's called constructive logic. The name is due to the fact that one must "construct" a proof, such as a function, in order to prove a theorem. Every theorem has an explicit construction which shows us how the proof is performed. This requirment, as it turns out, is quite so strict, so strict that we can no longer prove all the things we could in classical logic. In particular we will be unable to prove both $\lnot \lnot P \to P$ and $P \lor \lnot P$. Proving these clasically is trivial, just consider the case where $P$ is true, and the case where $P$ is false, in both cases these propositions hold. In Haskell however, it's trickier, think about it, how could one write these programs?
* Boolean logic is an oversimplification ```hs
* Broader logic needed, intutionistic logic impossible1 :: Not (Not a) -> a -- ((a -> Falsehood) -> Falsehood) -> a
impossible2 :: Either a (Not a) -- Either a (a -> Falsehood)
```
## The Horizon: Type theory These two propositions have names, $P \lor \lnot P$ is called the law of excluded middle, and $\lnot \lnot P \to P$ is called double negation. Though it might not be obvious, double negation actually follows from excluded middle:
* Quick recap, where does one go from here though? (överkurs) ```hs
* But how does one interpret higher order logic? assume_excluded_middle :: Either a (Not a)
* Pi and Sigma types assume_excluded_middle = error "Proof depends on excluded middle"
* Equality types?
-- Since there are no values of Falsehood this is a perfectly
-- fine definition, this cannot get stuck cause we cannot call it.
-- Proof-oriented programming languages almost always have a function
-- of this type.
if_pigs_fly :: Falsehood -> a
if_pigs_fly f = if_pigs_fly f
double_negation :: Not (Not a) -> a
double_negation notnota = case assume_excluded_middle of
Left a -> a
Right nota -> if_pigs_fly (notnota nota)
```
In Haskell our propositions are types, which carry proofs around, we cannot simply assume that any proposition must be true or false, because in doing so one would have to either produce a proof that it is true, or a proof that it is false. This is the very reason we are not able to prove excluded middle, as well as the reason that double negation follows from excluded middle. Excluded middle is the very rule telling us that we may assume every proposition is either true or false, we exclude the possiblity of a middle value.
Logicians have given a name to logics in which one cannot prove excluded middle, these logics are called intuitionistic. Initially it might be confusing why one would wish to work in a logic where not every proposition is true or false, such a fact seems obvious. Likewise, mathematicians have historically been [at each other arguing about the validity of excluded middle](https://en.wikipedia.org/wiki/Brouwer%E2%80%93Hilbert_controversy#Validity_of_the_law_of_excluded_middle). Thought it might seem counter-productive there are today a multitude of reasons to work without excluded middle. A philosiphical reason is provided by [one of Gödel's incompletness theorems](https://en.wikipedia.org/wiki/G%C3%B6del%27s_incompleteness_theorems#Completeness), which states that in all sufficiently powerful systems of logic there will be statements which are neither provable nor disprovable. In the presence of this knowledge, it might be unsettling to some that excluded middle lets one assume that these statements may be proven or disproven. Practically there are a lot of objects in modern mathematics which interpret intutionistic logic (such as Haskell!), meaning results in intutionistic logic give us results applying to more of mathematics. This is the true strength of intutionism, generality. An intutionistic proof holds classically, but a classical proof is not valid intutionistically.
## Wrapping up
If you've made it this far, then congratulations! Even though I've tried to make this blogpost introductory it's by no means trivial. Hopefully you are now feeling the same wonder as I did when stumbling into this topic. I'd like to end by broadly talking about where one might head to next from this wonderful crossroads of mathematics and computer science.
This blog post only covers propositional logic, but one can interpret predicate logic, and even higher order logic within programming languages. This is done with dependent type theory. In dependent type theories types may themselfs *depend* upon values, letting one create types such as `is-even n` which depent on a natural number `n`, which has as terms witnesses that `n` is even. These programming languages, or proof assistants as they are ususally called, allows one to prove properties of programs and mathematical objects. In doing so they provide a way to automatically check mathematical proofs for correctness. There are already many mathematicians using these tools to create formalized proofs of mathematical theorems.
If you are interested in learning more about dependent type theory, then you might be interested in downloading and playing around with one of these proof assistants. I personally recommend [agda](https://agda.readthedocs.io/en/latest/getting-started/installation.html) to those familiar with Haskell. The agda documentation includes a [list of tutorials](https://agda.readthedocs.io/en/latest/getting-started/tutorial-list.html). If you later wish to learn more about how doing math with types instead of sets might lead to new insights I encourage you to learn about homotopy type theory, for which there are some great resources: [HoTTEST Summer School 2022 lectures ](https://www.youtube.com/playlist?list=PLtIZ5qxwSNnzpNqfXzJjlHI9yCAzRzKtx), [HoTTEST Summer School 2022 Notes, Exercises, and Code](https://github.com/martinescardo/HoTTEST-Summer-School), [HoTT Book](https://homotopytypetheory.org/book/), [Egbert Rijkes HoTT intro book](https://github.com/EgbertRijke/HoTT-Intro) (note that this is an older version of Egberts Book, the final version is expected to be published soon), [1lab](https://1lab.dev/).
{% endkatexmm %} {% endkatexmm %}