4 ms·

Actually, it really seems equality has always been a bit hairy in mathematics, functional programming aside. It's just that trying to formalize it with construc

by aseipp 10y ago

Actually, it really seems equality has always been a bit hairy in mathematics, functional programming aside. It's just that trying to formalize it with constructive type theory sort of makes it much more clear how painful it is. :) But I don't really mean that "equality is fundamentally hard to compute because of functional programming" or anything. Rather, it might be the other way around: we haven't given a computational meaning to equality, which is why it's all so bad! It's more about equality is ugly at the moment and this results in some of that incidental complexity that I was talking about. To get rid of that ugliness, adopting equality as a computational thing is powerful! The notions of equivalence vs equals vs isomorphic, etc seem to get weird over time, at least in this amateur's mind. And that's not even getting into the problem that you have to establish "equalities" independent of the theory, which is part of, if not the, whole problem (e.g. in set theory, "a equals b" only makes sense once you establish an outside rule for what "equals" means. In HoTT, "equals" is not defined independently of the theory at all -- its in the same universe, so equality is "computational" on its own, in the sense you can talk about equalities, pass them around, and establish equalities between equalities, etcetera. This leads to the notion of infinity-groupoids, univalence, etc) Granted, it's not like the entire maths community is scrambling to fix this like the Manhattan project; but the notion of equality-being-hazy seems to be understood, even outside of functional formalisms. It seems to be more of a problem in higher order mathematics, too, which is where the majority of people who care about it work, it seems. While homotopy type theory is the current en-vogue approach to solving the hairy problems of equality (among other things) since it unifies all this... actually adding a computational interpretation is still an open question. So one problem is solved and another pops up, just as usual...

pron 10y ago
> The notions of equivalence vs equals vs isomorphic, etc seem to get weird over time Perhaps, but not for computation. There is a very clear, very nice, partial order on various kinds of computational semantics, and they all become a nice, "configurable" sliding scale once you work in a formalism that expresses computation more naturally than functions (that's because computations are simply not functions, at least not functions from the input to the output, and not even partial functions). Once you decide to work with functions you need to think of things like extensional vs. intensional equality etc., which simply aren't an issue in other formalisms. > It seems to be more of a problem in higher order mathematics, too. True, but the need for "higher-order mathematics" in the modeling of computation in the first place originates with the choice of functions as models of computation... Consider this: computation bears a lot of resemblance to continuous dynamical systems (computation is essentially a discrete dynamical process). Now, in (continuous) dynamical system, suppose you want to make your system "higher order": the derivative of the system will itself by a dynamical system. There is still no need to go higher-order mathematically; dynamical systems are usually represented as first order ODEs regardless of their conceptual "order". Instead, all you do is add another dimension to your state space. As the size of your state-vector is arbitrary, and as the mathematics of increasing it is very clear, all you need to do to "go deep" is "go wide". But perhaps I'm being unfair. While functions are not a very good abstraction for reasoning about computation, they are a very useful programming abstraction, and for end-to-end verification you must reason at the programming language level (although there may be better ways of doing that, too).
- aseipp 10y ago
  Ah, I see what you mean now -- yeah, if you simply don't work in the domain of dependent type theory but instead choose something more suitable, then it's not a problem, c.f. why I mentioned DTs still suffer from problems like equality being hairy. Not every approach is so unlucky. :) I thought you meant more generally in "general mathematics" where it does seem in some cases equality is kind of hazy, so I sort of misinterpreted. > True, but the need for higher-order mathematics in the modeling of computation in the first place originates with the choice of functions as models of computation... But perhaps I'm being unfair. While functions are not a very good abstraction for reasoning about computation, they are a very useful programming abstraction, and for end-to-end verification you must reason at the programming language level (although there may be better ways of doing that, too). I kind of left "higher order mathematics" a bit vague... Personally in all the proofs, etc I've needed you don't need to go as far as talking about topological spaces or n-categories or whatever, which is what I'd consider "higher order", but this is the space where a lot of the focus on wrangling equality, etc seems to come from, which is what I was getting at. Then again, most people using Coq heavily are probably exactly the people who care about this. :) I'm not one of those people, I just like programming. And personally I find the choice of functions, etc as a notion of computation quite powerful, even if it gets hairy sometimes! I suppose you could call it pidgeon-holing or laziness, but I tend to get a lot of insight from viewing mathematics from a computational, constructive point of view like this. I more use it as a "bridge" to get places rather than an overarching view of mathematics, I suppose, and I think it's quite useful at that (e.g. recently I found that I like the view of quotients in the computational, type-theoretic view rather than the 'quotients' of non-type-theory where you're really talking about partitions and equivalence classes, etc)... This is also probably partially due to the fact I've spent the majority of my programming career with systems like Haskell. So I'm fairly comfortable with "computational mathematics" from this POV.
  - pron 10y ago
    "Computational mathematics" is indeed very interesting (and lies at the very core of some type theories), but as a developer rather than a logician, I'm less concerned with the foundations of mathematics and more concerned with the opposite problem: mathematical computation, namely how computation is represented mathematically rather than how math is represented computationally. Functions are a fundamental mathematical abstraction, and requiring them to be computable is interesting, but functions are not a fundamental computational concept, and going the other way to represent computations as functions is what complicates matters when reasoning about many kinds of algorithms, especially those that are not mappings of inputs to outputs. In other words, I don't think that an interesting way to apply computational concepts (of typed lambda calculus) to the foundations of mathematics is necessarily the best way to apply mathematical thinking to computation. "Computational math" may not be the right math for "mathematical computation". There's an example of this unjustified (although possibly true -- we don't know) reasoning in the introduction to the Lean paper: > In practice, there is not a sharp distinction between verifying a piece of mathematics and verifying the correctness of a system: formal verification requires describing hardware and software systems in mathematical terms, at which point establishing claims as to their correctness becomes a form of theorem proving. Conversely, the proof of a mathematical theorem may require a lengthy computation, in which case verifying the truth of the theorem requires verifying that the computation does what it is supposed to do. The problem is that the kinds of computations relevant in the first case and the kinds of computation in the second case can be wildly different. Computations used in proofs are very much "functional" (map input to output). Computations in real-world software systems that really need formal verification rarely are. The most common type of computation in either category is the least common in the other, so the assumption that the same mathematical foundation (and/or the same tool) should be used for both is unjustified. While the authors use the term "in practice" to preface their statement, judging by their publication history, I'm a bit skeptical of their experience in verifying real-world software. Nevertheless, Lean does seem like a great way to learn about dependent types, and as you pointed out, the work on dependent types and their possible application in software verification is far from done, so it's very hard to judge at this point whether or not the direction is the right one. In the end, regardless of formalism, the proofs and techniques of software verification turn out to be very similar in all formalisms.

by aseipp 10y ago

pron 10y ago

> The notions of equivalence vs equals vs isomorphic, etc seem to get weird over time Perhaps, but not for computation. There is a very clear, very nice, partial order on various kinds of computational semantics, and they all become a nice, "configurable" sliding scale once you work in a formalism that expresses computation more naturally than functions (that's because computations are simply not functions, at least not functions from the input to the output, and not even partial functions). Once you decide to work with functions you need to think of things like extensional vs. intensional equality etc., which simply aren't an issue in other formalisms. > It seems to be more of a problem in higher order mathematics, too. True, but the need for "higher-order mathematics" in the modeling of computation in the first place originates with the choice of functions as models of computation... Consider this: computation bears a lot of resemblance to continuous dynamical systems (computation is essentially a discrete dynamical process). Now, in (continuous) dynamical system, suppose you want to make your system "higher order": the derivative of the system will itself by a dynamical system. There is still no need to go higher-order mathematically; dynamical systems are usually represented as first order ODEs regardless of their conceptual "order". Instead, all you do is add another dimension to your state space. As the size of your state-vector is arbitrary, and as the mathematics of increasing it is very clear, all you need to do to "go deep" is "go wide". But perhaps I'm being unfair. While functions are not a very good abstraction for reasoning about computation, they are a very useful programming abstraction, and for end-to-end verification you must reason at the programming language level (although there may be better ways of doing that, too).

aseipp 10y ago
Ah, I see what you mean now -- yeah, if you simply don't work in the domain of dependent type theory but instead choose something more suitable, then it's not a problem, c.f. why I mentioned DTs still suffer from problems like equality being hairy. Not every approach is so unlucky. :) I thought you meant more generally in "general mathematics" where it does seem in some cases equality is kind of hazy, so I sort of misinterpreted. > True, but the need for higher-order mathematics in the modeling of computation in the first place originates with the choice of functions as models of computation... But perhaps I'm being unfair. While functions are not a very good abstraction for reasoning about computation, they are a very useful programming abstraction, and for end-to-end verification you must reason at the programming language level (although there may be better ways of doing that, too). I kind of left "higher order mathematics" a bit vague... Personally in all the proofs, etc I've needed you don't need to go as far as talking about topological spaces or n-categories or whatever, which is what I'd consider "higher order", but this is the space where a lot of the focus on wrangling equality, etc seems to come from, which is what I was getting at. Then again, most people using Coq heavily are probably exactly the people who care about this. :) I'm not one of those people, I just like programming. And personally I find the choice of functions, etc as a notion of computation quite powerful, even if it gets hairy sometimes! I suppose you could call it pidgeon-holing or laziness, but I tend to get a lot of insight from viewing mathematics from a computational, constructive point of view like this. I more use it as a "bridge" to get places rather than an overarching view of mathematics, I suppose, and I think it's quite useful at that (e.g. recently I found that I like the view of quotients in the computational, type-theoretic view rather than the 'quotients' of non-type-theory where you're really talking about partitions and equivalence classes, etc)... This is also probably partially due to the fact I've spent the majority of my programming career with systems like Haskell. So I'm fairly comfortable with "computational mathematics" from this POV.
- pron 10y ago
  "Computational mathematics" is indeed very interesting (and lies at the very core of some type theories), but as a developer rather than a logician, I'm less concerned with the foundations of mathematics and more concerned with the opposite problem: mathematical computation, namely how computation is represented mathematically rather than how math is represented computationally. Functions are a fundamental mathematical abstraction, and requiring them to be computable is interesting, but functions are not a fundamental computational concept, and going the other way to represent computations as functions is what complicates matters when reasoning about many kinds of algorithms, especially those that are not mappings of inputs to outputs. In other words, I don't think that an interesting way to apply computational concepts (of typed lambda calculus) to the foundations of mathematics is necessarily the best way to apply mathematical thinking to computation. "Computational math" may not be the right math for "mathematical computation". There's an example of this unjustified (although possibly true -- we don't know) reasoning in the introduction to the Lean paper: > In practice, there is not a sharp distinction between verifying a piece of mathematics and verifying the correctness of a system: formal verification requires describing hardware and software systems in mathematical terms, at which point establishing claims as to their correctness becomes a form of theorem proving. Conversely, the proof of a mathematical theorem may require a lengthy computation, in which case verifying the truth of the theorem requires verifying that the computation does what it is supposed to do. The problem is that the kinds of computations relevant in the first case and the kinds of computation in the second case can be wildly different. Computations used in proofs are very much "functional" (map input to output). Computations in real-world software systems that really need formal verification rarely are. The most common type of computation in either category is the least common in the other, so the assumption that the same mathematical foundation (and/or the same tool) should be used for both is unjustified. While the authors use the term "in practice" to preface their statement, judging by their publication history, I'm a bit skeptical of their experience in verifying real-world software. Nevertheless, Lean does seem like a great way to learn about dependent types, and as you pointed out, the work on dependent types and their possible application in software verification is far from done, so it's very hard to judge at this point whether or not the direction is the right one. In the end, regardless of formalism, the proofs and techniques of software verification turn out to be very similar in all formalisms.