post haskell and logic
This commit is contained in:
parent
bb180bc6cb
commit
2d33d6dbb7
|
|
@ -1,154 +0,0 @@
|
|||
---
|
||||
layout: post
|
||||
title: "Haskell and Logic"
|
||||
---
|
||||
|
||||
Haskell programs are proofs, don't you know? Hidden inside the types of Haskell lies a deep connection to mathematical logic. Given some basic Haskell knowledge and mathematical interest you too may experience the sense of wonder I first did when discovering the Curry-Howard isomorphism.
|
||||
|
||||
<!--more-->
|
||||
|
||||
{% katexmm %}
|
||||
|
||||
## What is logic?
|
||||
|
||||
Before we can talk about logic in Haskell we have to talk about logic itself. While most of us have an intuition for what is logical it might be hard to formalise. This blog post will mainly concern itself with propositional logic. Propositional logic is made up by a set of rules telling us how to construct propositions, and how to derive conclusions from true propositions.
|
||||
|
||||
The following are some examples of propositions: "It is sunny outside", "The bank is open", "It is either sunny or rainy outside", "If it is rainy then the bank is not open". The first two statements are "atomic", they cannot be broken down into smaller propositions, unlike the latter two statements which are built up from smaller propositions. In addition to atoms there are the connectives 'and', 'or'; negation and implication. Additionally there is a true and a false proposition. Let us then specify which propositions we may form.
|
||||
|
||||
* The atomic propositions, which we will call $a, b, c \dots$
|
||||
* Truth and falsehood, written as $\top$ (truth) and $\bot$ (falsehood)
|
||||
* The connectives, which given any two propositions $P, Q$ lets us talk about
|
||||
* $P$ and $Q$ are true, written as $P \land Q$
|
||||
* $P$ or $Q$ (or both) are true, written as $P \lor Q$
|
||||
* Implication, which given any two propositions $P, Q$ lets us talk about
|
||||
* if $P$ is true then $Q$ is, written as $P \to Q$
|
||||
* Negation, which given a proposition $P$ lets us talk about
|
||||
* $P$ is false, written as $\lnot P$
|
||||
|
||||
Combining these we can create larger propositions such as $a \to a \lor b$ or $a \lor (b \land \lnot c)$. We can now translate English non-atomic propositions into the language of propositional logic. "If it is rainy then the bank is not open" becomes $\textrm{it is rainy} \to \lnot (\textrm{bank is open})$.
|
||||
|
||||
Now given the knowledge that a proposition $P$ is true, we can draw conclusions about the propositions used to construct $P$.
|
||||
|
||||
* If $P \land Q$ is true, then we know that both $P$ and $Q$ are 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 $\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.
|
||||
|
||||
When we are doing logic we are usually interested in proving that a proposition is either a tautology or a contradiction given a list of propositions declared to be true. One usually does this by following the rules of logic, which I have sketched out above, reaching conclusions based on hypotheses the hypotheses until one arrives at a conclusion. However, as I am about to show you, there is another way to do logic, through Haskell!
|
||||
|
||||
## Interpreting logic in Haskell
|
||||
|
||||
How does one begin to translate from propositional logic to Haskell? We will interpret propositions as types, and terms (elements) of a type as witnesses/proofs that the proposition is true. The computer typechecking our program will then serve as checking that our proof is correct, allowing us to automatically check if proofs are correct. While this might seem abstract at first it will become clear once you see how we translate propositions into Haskell.
|
||||
|
||||
Atomic propositions ($a,b,c,\dots$) are interpreted as type variables `a`, `b`, `c`, etc. You might notice that there is no way to prove `a`. This is because to prove `a` in Haskell we have to create some proof `p :: a`, but since `a` could be any type we have no way of doing this. This corresponds to how cannot prove or disprove atomic propositions without drawing conclusion from other propositions in classical logic.
|
||||
|
||||
$\top$ may be interpreted as any type which we know a term of. For the sake of readability we define our own truth type, with a single constructor bearing witness to its truth:
|
||||
```hs
|
||||
data Truth = TruthWitness
|
||||
```
|
||||
Translating $\bot$ might seem more tricky, but it turns out Haskell actually lets us define empty types without constructors, that is, a proposition with no proof. We thus define the following:
|
||||
```hs
|
||||
data Falsehood
|
||||
```
|
||||
|
||||
The connectives might seem more tricky, but turn out to be fairly straight forward as well. A proof of $P \land Q$ is simply a proof of $P$ and a proof of $Q$, but wait, that's a pair! $P \land Q$ is then interpreted as `(P, Q)`. Likewise a proof of $P \lor Q$ is *either* a proof of $P$ or a proof of $Q$, that's right, it's the `Either` type! $P \lor Q$ is interpreted as `Either P Q`.
|
||||
|
||||
The implication $P \to Q$ tells us that if we have a proof of $P$ then we have a proof of $Q$. So what we need is a way of turning terms of type $P$ into terms of type $Q$. We need a function `P -> Q`, and would you look at that, it's even the same arrow!
|
||||
|
||||
Perhaps surprisingly negation is the trickiest part of the translation. For $\lnot P$ to be true $P$ must be false, that is, there are no terms `p :: P` bearing witness to the truth of P. How can we express this within Haskell? The trick is to redefine $\lnot P$ as $P \to \bot$, that is, $\bot$ is true if $P$ is. But since we *know* that $\bot$ is false, this means $P$ cannot be true. Thus we interpret $\lnot P$ as `P -> Falsehood`. In order to aid readability we will make the following definition:
|
||||
```
|
||||
type Not p = p -> Falsehood
|
||||
```
|
||||
|
||||
Now that we've introduced our language, let us speak! We shall prove the above mentioned tautology $a -> a \lor b$, by constructing a function `a -> Either a b`. If you've used the `Either` type before then the proof is trivial.
|
||||
```hs
|
||||
proof1 :: a -> Either a b
|
||||
proof1 = Left
|
||||
```
|
||||
|
||||
Now let us prove that $a \land \lnot a$ is a contradiction, we shall do this by proving $\lnot (a \land \lnot a)$. In doing so we need to construct a term of type `Not (a, Not a)`, which after we unwrap the definition of `Not` becomes `(a, a -> Falsehood) -> Falsehood`. Thus, we must construct a function to `Falsehood`, which has no inhabitants, however, we are given a function `a -> Falsehood` which we may use to get a term of the empty `Falsehood` type, by applying the supplied value of type `a` to it.
|
||||
```hs
|
||||
proof2 :: Not (a, Not a) -- (a, a -> Falsehood) -> Falsehood)
|
||||
proof2 (a, f) = f a
|
||||
```
|
||||
|
||||
I strongly encourage you to play around with this on your own, trying to come up with some propositions and proving them by hand and with Haskell. The table below is gives an overview of the translation.
|
||||
|
||||
<table>
|
||||
<tr> <th>Logic</th> <th>Haskell</th> </tr>
|
||||
<tr> <td>Proposition</td> <td>Type</td> </tr>
|
||||
<tr> <td>Proof</td> <td>Term (element of type)</td> </tr>
|
||||
<tr> <td>Atom</td> <td>Type variable</td> </tr>
|
||||
<tr> <td>$\top$</td> <td>Type with known term</td> </tr>
|
||||
<tr> <td>$\bot$</td> <td>Type with no terms</td> </tr>
|
||||
<tr> <td>$P \land Q$</td> <td><code>(P, Q)</code></td> </tr>
|
||||
<tr> <td>$P \lor Q$</td> <td><code>Either P Q</code></td> </tr>
|
||||
<tr> <td>$P \to Q$</td> <td><code>P -> Q</code></td> </tr>
|
||||
<tr> <td>$\lnot P$</td> <td><code>P -> EmptyType</code></td> </tr>
|
||||
</table>
|
||||
|
||||
|
||||
## The paradoxes of Haskell
|
||||
|
||||
I admit, we did use a little too much effort in the previous section when constructing `proof2`, here is a more succinct version, which type checks all the same:
|
||||
```hs
|
||||
proof2 :: Not (a, Not a) -- (a, a -> Falsehood) -> Falsehood)
|
||||
proof2 = undefined
|
||||
```
|
||||
And here's another version
|
||||
```hs
|
||||
proof2 :: Not (a, Not a) -- (a, a -> Falsehood) -> Falsehood)
|
||||
proof2 = proof2
|
||||
```
|
||||
While all of these typecheck we understand that they are not valid proofs, in fact we could prove `Falsehood` in this exact way.
|
||||
```
|
||||
proof3 :: Falsehood
|
||||
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.
|
||||
|
||||
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.
|
||||
|
||||
## Excluding the middle
|
||||
|
||||
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?
|
||||
```hs
|
||||
impossible1 :: Not (Not a) -> a -- ((a -> Falsehood) -> Falsehood) -> a
|
||||
impossible2 :: Either a (Not a) -- Either a (a -> Falsehood)
|
||||
```
|
||||
|
||||
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:
|
||||
|
||||
```hs
|
||||
assume_excluded_middle :: Either a (Not a)
|
||||
assume_excluded_middle = error "Proof depends on excluded middle"
|
||||
|
||||
-- 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 %}
|
||||
154
_posts/2022-12-15-haskell-and-logic.md
Normal file
154
_posts/2022-12-15-haskell-and-logic.md
Normal file
|
|
@ -0,0 +1,154 @@
|
|||
---
|
||||
layout: post
|
||||
title: "Haskell and Logic"
|
||||
---
|
||||
|
||||
Haskell programs are proofs, don't you know? Hidden inside the types of Haskell lies a deep connection to mathematical logic. Given some basic Haskell knowledge and mathematical interest, you too may experience the sense of wonder I first did when discovering the Curry-Howard isomorphism.
|
||||
|
||||
<!--more-->
|
||||
|
||||
{% katexmm %}
|
||||
|
||||
## What is logic?
|
||||
|
||||
Before we can talk about logic in Haskell we have to talk about propositional logic. Propositional logic is a set of rules telling us how to construct propositions, and how to derive conclusions from true ones.
|
||||
|
||||
First, we shall get a feel for what a proposition is by breaking down some examples. Consider the following statements: "It is sunny outside", "The bank is open", "It is either sunny or rainy outside", and "If it is rainy then the bank is not open". The first two statements are "atomic", they cannot be broken down into smaller propositions, unlike the latter two statements which are built up from smaller propositions. Let us then specify the forms a propositions may have.
|
||||
|
||||
* The atomic propositions, which we shall call $a, b, c \dots$
|
||||
* Truth and falsehood, written as $\top$ (truth) and $\bot$ (falsehood)
|
||||
* The connectives, given two propositions $P, Q$ lets us talk about
|
||||
* $P$ and $Q$ are true, written as $P \land Q$
|
||||
* $P$ or $Q$ (or both) are true, written as $P \lor Q$
|
||||
* Implication, given two propositions $P, Q$ lets us talk about
|
||||
* if $P$ is true then $Q$ is, written as $P \to Q$
|
||||
* Negation, which given a proposition $P$ lets us talk about
|
||||
* $P$ is false, written as $\lnot P$
|
||||
|
||||
Combining these we can create larger propositions such as $a \to a \lor b$ or $a \lor (b \land \lnot c)$. We can now translate English non-atomic propositions into the language of propositional logic. "If it is rainy then the bank is not open" becomes $\textrm{it is rainy} \to \lnot (\textrm{bank is open})$.
|
||||
|
||||
Given the knowledge that a proposition $P$ is true, we may make conclusions about the propositions used to construct $P$.
|
||||
|
||||
* If $P \land Q$ is true, then both $P$ and $Q$ are true
|
||||
* If $P \lor Q$ is true, then at least one of $P$ or $Q$ is true
|
||||
* If $P \to Q$ is true, then $Q$ must be true whenever $P$ is
|
||||
* If $\lnot P$ is true, then $P$ is false
|
||||
|
||||
To prove things one more concept needs to be introduced, that of tautologies and contradictions. A tautology is a statement that is true no matter if the atoms inside of it are true or not, and conversely, a contradiction is a statement that 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 ourselves with the motive of the implication. An important tautology following the same reasoning is $\bot \to P$. An example of a contradiction is $a \land \lnot a$, this proposition states that $a$ is both true and false, which is impossible.
|
||||
|
||||
In logic we are usually interested in proving that a proposition is either a tautology or a contradiction, proving or disproving its truth. One usually does this by following the rules of the logic, repeatedly applying them to yield a proof. However there is another way to do logic, through Haskell!
|
||||
|
||||
## Interpreting logic in Haskell
|
||||
|
||||
How does one translate from propositional logic to Haskell? We shall interpret types as propositions, and terms (elements) of a type as witnesses or proofs that the proposition (the type they inhabit) is true. The typechecking of Haskell will then double as a proof checker. This might seem abstract at first, but once you see how the building blocks of propositions translate into types it will become clear.
|
||||
|
||||
Atomic propositions ($a,b,c,\dots$) are interpreted as type variables `a`, `b`, `c`, etc. You might notice that there is no way to prove `a`, since one would have to create a proof `p :: a`, that is, a term inhabiting every type. This corresponds to how one cannot prove or disprove atomic propositions in propositional logic.
|
||||
|
||||
$\top$ may be interpreted as any type of which we know a term, that is, any proposition of which we know a proof. For the sake of readability we shall define a truth type, with a single constructor bearing witness to its truth.
|
||||
```hs
|
||||
data Truth = TruthWitness
|
||||
```
|
||||
Translating $\bot$ might seem more tricky, but it turns out Haskell lets us define empty types without constructors, that is, a proposition with no proof. We thus define the following.
|
||||
```hs
|
||||
data Falsehood
|
||||
```
|
||||
|
||||
The connectives might seem more tricky, but turn out to be fairly straightforward as well. A proof of $P \land Q$ is simply a proof of $P$ and a proof of $Q$, but wait, that's a pair! $P \land Q$ is thus interpreted as `(P, Q)`. Likewise, a proof of $P \lor Q$ is *either* a proof of $P$ or a proof of $Q$, that's right, it's the `Either` type! $P \lor Q$ is interpreted as `Either P Q`.
|
||||
|
||||
The implication $P \to Q$ tells us that if we have a proof of $P$ then we have a proof of $Q$. So what we need is a way of turning terms of type $P$ into terms of type $Q$. That is, a function `P -> Q`, would you look at that, it's even the same arrow!
|
||||
|
||||
Perhaps surprisingly the trickiest part of the translation is negation. For $\lnot P$ to be true $P$ must be false, that is, there may not be any terms `p :: P` bearing witness to the truth of P. How can we express this within Haskell? The trick is to redefine $\lnot P$ as $P \to \bot$, that is, $\bot$ is true if $P$ is. But since we *know* that $\bot$ is false, this means $P$ cannot be true. Thus we interpret $\lnot P$ as `P -> Falsehood`. To aid readability we will make the definition below.
|
||||
```hs
|
||||
type Not p = p -> Falsehood
|
||||
```
|
||||
|
||||
Now that we've introduced our language, let us speak! We shall prove the above-mentioned tautology $a \to a \lor b$ by constructing a function `a -> Either a b`. If you've used the `Either` type before then the proof is trivial.
|
||||
```hs
|
||||
proof1 :: a -> Either a b
|
||||
proof1 = Left
|
||||
```
|
||||
|
||||
Now let us prove that $a \land \lnot a$ is a contradiction, we shall do this by proving its negation $\lnot (a \land \lnot a)$. In doing so we need to construct a term of type `Not (a, Not a)`, that is, `(a, a -> Falsehood) -> Falsehood`. Thus, we must construct a function to `Falsehood` which has no inhabitants, however, we are given a function `a -> Falsehood` which we may use to get a term of the empty `Falsehood` type by applying the supplied value of type `a` to it.
|
||||
```hs
|
||||
proof2 :: Not (a, Not a) -- (a, a -> Falsehood) -> Falsehood)
|
||||
proof2 (a, f) = f a
|
||||
```
|
||||
|
||||
I strongly encourage you to play around with this on your own, coming up with some propositions and proving them by hand and using Haskell. The table below gives an overview of the translation from logic to Haskell.
|
||||
|
||||
<table>
|
||||
<tr> <th>Logic</th> <th>Haskell</th> </tr>
|
||||
<tr> <td>Proposition</td> <td>Type</td> </tr>
|
||||
<tr> <td>Proof</td> <td>Term (element of type)</td> </tr>
|
||||
<tr> <td>Atom</td> <td>Type variable</td> </tr>
|
||||
<tr> <td>$\top$</td> <td>Type with a known term</td> </tr>
|
||||
<tr> <td>$\bot$</td> <td>Type with no terms</td> </tr>
|
||||
<tr> <td>$P \land Q$</td> <td><code>(P, Q)</code></td> </tr>
|
||||
<tr> <td>$P \lor Q$</td> <td><code>Either P Q</code></td> </tr>
|
||||
<tr> <td>$P \to Q$</td> <td><code>P -> Q</code></td> </tr>
|
||||
<tr> <td>$\lnot P$</td> <td><code>P -> EmptyType</code></td> </tr>
|
||||
</table>
|
||||
|
||||
|
||||
## The paradoxes of Haskell
|
||||
|
||||
I admit, we did use a little too much effort when constructing `proof2`, there is a more succinct version, which type checks all the same.
|
||||
```hs
|
||||
proof2 :: Not (a, Not a) -- (a, a -> Falsehood) -> Falsehood)
|
||||
proof2 = undefined
|
||||
```
|
||||
And here's another version!
|
||||
```hs
|
||||
proof2 :: Not (a, Not a) -- (a, a -> Falsehood) -> Falsehood)
|
||||
proof2 = proof2
|
||||
```
|
||||
While both of these typecheck, we understand that they are not valid proofs, in fact, we can prove `Falsehood` in this exact way.
|
||||
```hs
|
||||
proof3 :: Falsehood
|
||||
proof3 = proof3
|
||||
```
|
||||
This is not good, maybe programming languages don't correspond to logic after all? The solution is to "run" our proofs 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.
|
||||
|
||||
The programming languages studied by logicians 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 to model non-terminating programs). These programming languages, while they can check proofs entirely during typechecking, come with their 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 in order to garantuee termination. Consequently, these languages are not [Turing-complete](https://en.wikipedia.org/wiki/Turing_completeness), meaning there are programs one cannot write in the language.
|
||||
|
||||
## Excluding the middle
|
||||
|
||||
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 that shows us how the proof is performed. This requirement, as it turns out, is quite 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 classically 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?
|
||||
```hs
|
||||
impossible1 :: Not (Not a) -> a -- ((a -> Falsehood) -> Falsehood) -> a
|
||||
impossible2 :: Either a (Not a) -- Either a (a -> Falsehood)
|
||||
```
|
||||
|
||||
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 follows from excluded middle. By assuming excluded middle, we can even use Haskell to prove this.
|
||||
|
||||
```hs
|
||||
assume_excluded_middle :: Either a (Not a)
|
||||
assume_excluded_middle = error "Proof depends on excluded middle"
|
||||
|
||||
-- Since there are no values of Falsehood this is a perfectly
|
||||
-- fine constructive definition. One cannot call this function
|
||||
-- without already using an error or infinite loop.
|
||||
-- Proof-oriented programming languages will let you construct
|
||||
-- a function of this type without using `error`.
|
||||
if_pigs_fly :: Falsehood -> a
|
||||
if_pigs_fly f = error "cannot happen"
|
||||
|
||||
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, excluding the possibility 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 may be assumed to be either true or false, such a fact seems obvious. Likewise, mathematicians have historically been [at each other arguing over the validity of excluded middle](https://en.wikipedia.org/wiki/Brouwer%E2%80%93Hilbert_controversy#Validity_of_the_law_of_excluded_middle). Though intuitionistic logic might seem counter-productive there are today multitudes of reasons to work without excluded middle. A philosophical reason is provided by [Gödel's incompleteness theorem](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 that are neither provable nor disprovable. In the presence of this knowledge, it might be unsettling that excluded middle lets one assume these statements are either true or false. There are also practical reasons to work in intuitionistic logic. There are a lot of objects in mathematics that interpret intuitionistic logic (such as Haskell), meaning results in intuitionistic logic apply to more of mathematics. Generality is the true strength of intuitionism. An intuitionistic proof holds in a classical setting, but a classical proof may not be interpreted intuitionistically.
|
||||
|
||||
## Wrapping up
|
||||
|
||||
If you've made it this far, then congratulations! Even though I've tried to make this blog post 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 writing about where one might head next.
|
||||
|
||||
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 themselves *depend* upon values, letting one create types such as `is-even n` which depend on a natural number `n`. This type would have terms which are witnesses that `n` is even. These programming languages, or proof assistants as they are usually called, enable you to prove properties of both 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 a proof assistant. I recommend [agda](https://agda.readthedocs.io/en/latest/getting-started/installation.html) to those familiar with Haskell; a lengthy [list of agda tutorials](https://agda.readthedocs.io/en/latest/getting-started/tutorial-list.html) is included in its documentation. If you wish to learn more about how doing math with types rather than sets might lead to new insights and connections to topology, then 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 GitHub](https://github.com/martinescardo/HoTTEST-Summer-School), [1lab](https://1lab.dev/1Lab.intro.html), [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).
|
||||
|
||||
{% endkatexmm %}
|
||||
Loading…
Reference in New Issue
Block a user