6 ms·

Constructive mathematics and computer programming (1979) [pdf]

130 points by mathetic 7y ago

AnthonBerg 7y ago
Per Martin-Löf writes so beautifully. Here’s more: https://github.com/michaelt/martin-lof https://github.com/michaelt/martin-lof Here’s another one - this one is wonderful: https://archive-pml.github.io/martin-lof/pdfs/Bibliopolis-Book-retypeset-1984.pdf https://archive-pml.github.io/martin-lof/pdfs/Bibliopolis-Bo... As far as I understand the theory, then dependently typed languages such as Idris have their roots in his work on intuitionistic type theory: https://en.wikipedia.org/wiki/Intuitionistic_type_theory https://en.wikipedia.org/wiki/Intuitionistic_type_theory Intuitionism in math is beautiful imo: https://en.wikipedia.org/wiki/Intuitionism https://en.wikipedia.org/wiki/Intuitionism
- jhedwards 7y ago
  Out of curiosity as someone less mathematically inclined but very interested in mathematics: what do you do with the equations in books like this? Do you look at them and already intuitively know what they mean so you don't have to dig deeper? Do you slowly go over each element individually and then grasp the whole thing afterwards? Or are you so used to them that you can read them more or less the way you read English? I really want go deeper into this stuff but when I look at these books I feel like I would need years of specialized training to understand them.
  - intuitionist 7y ago
    Written mathematics is quite informationally dense and, in general, reads much more slowly than typical English prose. Sometimes you do have to go over an equation symbol-by-symbol; sometimes you have to convince yourself of the truth of a sentence with no symbols at all. In this particular case, though, you're in luck, as Martin-Löf gave a less technical and more philosophical series of lectures on the same subject, which are a much easier read: http://archive-pml.github.io/martin-lof/pdfs/Meanings-of-the-Logical-Constants-1983.pdf http://archive-pml.github.io/martin-lof/pdfs/Meanings-of-the...
  - hackermailman 7y ago
    Disclaimer: I am a self taught pleb, not a mathematician. The pdf blows up my phone but the first equations look like basic calculus, and the rest seem to be in the form of logical judgments where above the horizontal line are called the premises of the rule, and the judgment below the line is called its conclusion. I've seen Godel's T (System T) used in this style, and it seems this pdf is using set theory (again, my shit phone explodes and can't load half the pages) though I would imagine these would be done in category theory these days. To "understand" math, (scare quotes because again, I'm just a pleb), you really need to know what field, or set of axioms, or universe you're working in. The rational numbers are the easiest imho, when you get into the reals you're dealing with mathematical objects that may not even be possible to be represented as numbers (as I understand it) so if you can understand symbolic programming ala Sussman Lisp/Scheme you can understand math just you're unfamiliar with the notation, and unfamilar with whatever the rules of this particular abstraction are, that's all. By axioms I mean somebody has merely stated "I created this universe, here are the axioms that rule this abstract universe" meaning they often will not be congruent with any kind of other fields/axioms, in my experience as a plebmatician. If you want to understand there's a guy from here who wrote a book https://pimbook.org/ https://pimbook.org/ and to get into Per Martin-Löf you'll probably need some logic courses, professor Robert Harper or Frank Pfenning both have 'intuitionistic' constructivist math resources you can read/learn from if you google.
  - AnthonBerg 7y ago
    I had exactly the same question. Until just last year. (I’m 39.) We’re all different, especially in how we process abstract concepts. I process them quite visually. Among my friends it seems there is some correlation between having a maths degree and thinking directly in the math symbols. What I have tried to do is just to power through. Scanning and jumping over the paper I try to construct a mental model that the equation is a blueprint for. This is this. This is that. There’s a relation here. What is it. Ah yes it’s just that here. And that is then ... yes. Usually when i get the equation it’s much simpler than I assume at first. It’s just the ideas in a couple of paragraphs put together in an unambiguous way. So I just kind of power through! And it can and does take some time! But once through it tends to stick. it’s quite cool.
r00tanon 7y ago
Very interesting. Amazing how much we owe, without realizing, to the early pioneers and designers of the first computers, who often prognosticated issues we deal with today. I recently have been researching Leslie Lamport's TLA+ project. Definitely in line with the ideas in this paper. https://lamport.azurewebsites.net/tla/tla.html https://lamport.azurewebsites.net/tla/tla.html
- auggierose 7y ago
  Nah, no! Leslie Lamport is quite far away from constructive mathematics. You will for example see his explanation of logic in the TLA+ video lectures is entirely classical.
codedrome 7y ago
Thanks, I'll copy this to my tablet so I can carry it around with me. Looking forward to being impressed (hopefully) that it is still relevant today.
- AnthonBerg 7y ago
  That paper is still the future, it looks like to me.
ex3xu 7y ago
As a layman I'm curious about the state of constructivist mathematics and intuitionism since the tragic passing of Vladimir Voevodsky in 2017. I recall reading about the Coq proof assistant, homotopy type theory, and univalent foundations with some interest, but I haven't been keeping up with any new developments -- is it still an active field of research? I'm also curious if someone can weigh in on the fact that this paper by Martin-Löf finishes with a proof of the axiom of choice -- isn't that a bit of a controversial axiom? Does all of constructivist mathematics still depend on the axiom of choice to this day?
- garmaine 7y ago
  I think you have it backwards? From a mathematical perspective, the constructivist framework is defined as "provable without the axiom of choice." Constructivists are very concerned with avoiding the axiom of choice.
  - ex3xu 7y ago
    You're right. Wikipedia mentions that Voevodsky's model is considered to be non-constructive since it uses the axiom of choice in an ineliminable way. > The problem of finding a constructive interpretation of the rules of the Martin-Löf type theory that in addition satisfies the univalence axiom and canonicity for natural numbers remains open. A partial solution is outlined in a paper by Marc Bezem, Thierry Coquand and Simon Huber[17] with the key remaining issue being the computational property of the eliminator for the identity types. The ideas of this paper are now being developed in several directions including the development of the cubical type theory. I'm getting confused because Martin-Lof writes at the end of this paper: > I shall construct an object of this type, an object which may at the same time be interpreted as a proof of the axiom of choice... Thus (Az)((..tx)p(z(x)), (lx)q(z(x))) is the sought for proof of the axiom of choice.
    - tines 7y ago
      I'm confused then because the paper linked in the OP states: > The true source of uncomputeable functions is not the axiom if choice (which is valid intuitionistically) but the law of the excluded middle and indirect proof [emphasis original]
ukj 7y ago
Few years ago I joined some metaphysical dots between "construction", "constructivism", "creation" and "creationism" in my head, which is what led me on to explore 100 years of history/theory behind computational trinitarianism, intuitionistic logic, Curry-Howard isomorphism etc. This conceptual understanding of Monist metaphysics was the end of my militant atheism. The expression of knowledge is the creation of knowledge. It pleases me to see that Per Martin-Löf joined the same dots in his paper "A path from logic to metaphysics".

130 points by mathetic 7y ago

Per Martin-Löf writes so beautifully. Here’s more: https://github.com/michaelt/martin-lof https://github.com/michaelt/martin-lof Here’s another one - this one is wonderful: https://archive-pml.github.io/martin-lof/pdfs/Bibliopolis-Book-retypeset-1984.pdf https://archive-pml.github.io/martin-lof/pdfs/Bibliopolis-Bo... As far as I understand the theory, then dependently typed languages such as Idris have their roots in his work on intuitionistic type theory: https://en.wikipedia.org/wiki/Intuitionistic_type_theory https://en.wikipedia.org/wiki/Intuitionistic_type_theory Intuitionism in math is beautiful imo: https://en.wikipedia.org/wiki/Intuitionism https://en.wikipedia.org/wiki/Intuitionism

jhedwards 7y ago
Out of curiosity as someone less mathematically inclined but very interested in mathematics: what do you do with the equations in books like this? Do you look at them and already intuitively know what they mean so you don't have to dig deeper? Do you slowly go over each element individually and then grasp the whole thing afterwards? Or are you so used to them that you can read them more or less the way you read English? I really want go deeper into this stuff but when I look at these books I feel like I would need years of specialized training to understand them.
- intuitionist 7y ago
  Written mathematics is quite informationally dense and, in general, reads much more slowly than typical English prose. Sometimes you do have to go over an equation symbol-by-symbol; sometimes you have to convince yourself of the truth of a sentence with no symbols at all. In this particular case, though, you're in luck, as Martin-Löf gave a less technical and more philosophical series of lectures on the same subject, which are a much easier read: http://archive-pml.github.io/martin-lof/pdfs/Meanings-of-the-Logical-Constants-1983.pdf http://archive-pml.github.io/martin-lof/pdfs/Meanings-of-the...
- hackermailman 7y ago
  Disclaimer: I am a self taught pleb, not a mathematician. The pdf blows up my phone but the first equations look like basic calculus, and the rest seem to be in the form of logical judgments where above the horizontal line are called the premises of the rule, and the judgment below the line is called its conclusion. I've seen Godel's T (System T) used in this style, and it seems this pdf is using set theory (again, my shit phone explodes and can't load half the pages) though I would imagine these would be done in category theory these days. To "understand" math, (scare quotes because again, I'm just a pleb), you really need to know what field, or set of axioms, or universe you're working in. The rational numbers are the easiest imho, when you get into the reals you're dealing with mathematical objects that may not even be possible to be represented as numbers (as I understand it) so if you can understand symbolic programming ala Sussman Lisp/Scheme you can understand math just you're unfamiliar with the notation, and unfamilar with whatever the rules of this particular abstraction are, that's all. By axioms I mean somebody has merely stated "I created this universe, here are the axioms that rule this abstract universe" meaning they often will not be congruent with any kind of other fields/axioms, in my experience as a plebmatician. If you want to understand there's a guy from here who wrote a book https://pimbook.org/ https://pimbook.org/ and to get into Per Martin-Löf you'll probably need some logic courses, professor Robert Harper or Frank Pfenning both have 'intuitionistic' constructivist math resources you can read/learn from if you google.
- AnthonBerg 7y ago
  I had exactly the same question. Until just last year. (I’m 39.) We’re all different, especially in how we process abstract concepts. I process them quite visually. Among my friends it seems there is some correlation between having a maths degree and thinking directly in the math symbols. What I have tried to do is just to power through. Scanning and jumping over the paper I try to construct a mental model that the equation is a blueprint for. This is this. This is that. There’s a relation here. What is it. Ah yes it’s just that here. And that is then ... yes. Usually when i get the equation it’s much simpler than I assume at first. It’s just the ideas in a couple of paragraphs put together in an unambiguous way. So I just kind of power through! And it can and does take some time! But once through it tends to stick. it’s quite cool.

r00tanon 7y ago

Very interesting. Amazing how much we owe, without realizing, to the early pioneers and designers of the first computers, who often prognosticated issues we deal with today. I recently have been researching Leslie Lamport's TLA+ project. Definitely in line with the ideas in this paper. https://lamport.azurewebsites.net/tla/tla.html https://lamport.azurewebsites.net/tla/tla.html

auggierose 7y ago
Nah, no! Leslie Lamport is quite far away from constructive mathematics. You will for example see his explanation of logic in the TLA+ video lectures is entirely classical.

codedrome 7y ago

Thanks, I'll copy this to my tablet so I can carry it around with me. Looking forward to being impressed (hopefully) that it is still relevant today.

AnthonBerg 7y ago
That paper is still the future, it looks like to me.

ex3xu 7y ago

As a layman I'm curious about the state of constructivist mathematics and intuitionism since the tragic passing of Vladimir Voevodsky in 2017. I recall reading about the Coq proof assistant, homotopy type theory, and univalent foundations with some interest, but I haven't been keeping up with any new developments -- is it still an active field of research? I'm also curious if someone can weigh in on the fact that this paper by Martin-Löf finishes with a proof of the axiom of choice -- isn't that a bit of a controversial axiom? Does all of constructivist mathematics still depend on the axiom of choice to this day?

garmaine 7y ago
I think you have it backwards? From a mathematical perspective, the constructivist framework is defined as "provable without the axiom of choice." Constructivists are very concerned with avoiding the axiom of choice.
- ex3xu 7y ago
  You're right. Wikipedia mentions that Voevodsky's model is considered to be non-constructive since it uses the axiom of choice in an ineliminable way. > The problem of finding a constructive interpretation of the rules of the Martin-Löf type theory that in addition satisfies the univalence axiom and canonicity for natural numbers remains open. A partial solution is outlined in a paper by Marc Bezem, Thierry Coquand and Simon Huber[17] with the key remaining issue being the computational property of the eliminator for the identity types. The ideas of this paper are now being developed in several directions including the development of the cubical type theory. I'm getting confused because Martin-Lof writes at the end of this paper: > I shall construct an object of this type, an object which may at the same time be interpreted as a proof of the axiom of choice... Thus (Az)((..tx)p(z(x)), (lx)q(z(x))) is the sought for proof of the axiom of choice.
  - tines 7y ago
    I'm confused then because the paper linked in the OP states: > The true source of uncomputeable functions is not the axiom if choice (which is valid intuitionistically) but the law of the excluded middle and indirect proof [emphasis original]

ukj 7y ago

Few years ago I joined some metaphysical dots between "construction", "constructivism", "creation" and "creationism" in my head, which is what led me on to explore 100 years of history/theory behind computational trinitarianism, intuitionistic logic, Curry-Howard isomorphism etc. This conceptual understanding of Monist metaphysics was the end of my militant atheism. The expression of knowledge is the creation of knowledge. It pleases me to see that Per Martin-Löf joined the same dots in his paper "A path from logic to metaphysics".