2 ms·

> OK, well, that was far from clear. Here's your original question: Yeah, sorry about that - not being an academic myself makes it hard to put it across in the

> OK, well, that was far from clear. Here's your original question: Yeah, sorry about that - not being an academic myself makes it hard to put it across in the correct way. > No on has found a breakthrough in these woods, and there are good reasons to believe there is none to be found That's absolutely fine by me - I'm not looking to break through the undecidability barrier, only to implement an algorithm that can prove theorems we already know are decidable (well, group functions into the always halts/doesn't always halt/undecidable categories). The numerous branching and totally equivalent fields is the thing I'm wary of - I don't want to have to invest 6 months learning category theory, only to find out that what I want to do is better expressed by type theory or second order logic or something else entirely. I guess in my mind it's similar to building a complex application in one programming language just to discover certain patterns can't be idiomatically expressed in that language, so you have to write horrible hacks to compensate for that lacking where you could have chosen a different language in the first place. From my own research I'm leaning towards axiom systems, perhaps utilising Zermelo-Fraenkel set theory as a basis. I don't know, it's early days yet. I'll keep reading and get a rough grasp on the principal fields before I make a definitive decision.

lisper 8y ago
> I'm not looking to break through the undecidability barrier That, too, was far from clear. You said you were tackling this problem: > what is the property of a program that makes it undecidable? and I told you: > That is itself an undecidable question! and explained why (at least three times). And AFAICT you still don't get it because you still say you want to: > implement an algorithm that can prove theorems we already know are decidable (well, group functions into the always halts/doesn't always halt/undecidable categories) and that is the problem of automated theorem proving, which is an open research issue, and (provably) always will be. If you want to get a small taste of what you're up against, try proving that this program always halts: f(x:int, y:int) = ( x+y == y+x ? halt : loop ) In other words, try proving the commutative law of addition. If you get that, try to prove that this lambda-calculus expression (λ (n f) (n (λ (c i) (i (c (λ (f x) (i f (f x))))))(λ x f) (λ x x))) computes a factorial expressed as a Church numeral. (See http://www.flownet.com/ron/lambda-calculus.html http://www.flownet.com/ron/lambda-calculus.html for some hints.) And that's just what you get from elementary arithmetic. If you really want to blow your mind, look at: http://www.mrob.com/pub/math/largenum.html http://www.mrob.com/pub/math/largenum.html and the associated software: http://www.mrob.com/pub/perl/hypercalc.html http://www.mrob.com/pub/perl/hypercalc.html Once you get to infinity you are only just getting started: https://johncarlosbaez.wordpress.com/2016/06/29/large-countable-ordinals-part-1/ https://johncarlosbaez.wordpress.com/2016/06/29/large-counta... And even all that is just what you get from discrete math! Then there's calculus, topology, algebraic varieties (of which elliptic curves are one example, and even that is a whole field of study). And even here we've not even begun to scratch the surface of what is possible. The world of math is (provably!) richer than you -- or anyone -- can possibly imagine! That's what "undecidable" means. Your only reasonable hope of making any kind of non-trivial progress is to focus on one domain, and then use the constraints imposed by the properties of that domain to shrink the problem down to something potentially manageable.
- beaconstudios 8y ago
  See, I'm not an academic - proving that addition is commutative is not in scope for what I'm wanting to do. It is not a big leap for me to make that an axiom in my system, I'm almost entirely disinterested in trying to innovate in the pure theory of foundational mathematics. I find the theory itself extremely interesting but that's just not my path. I thought I was clear about what I was wanting to build - a practical system for categorising functions that can be shown to halt or not always halt, lumping everything else into a third category. Academia and pure maths just isn't for me, this is so I can build a language with minimal bugs.
  - lisper 8y ago
    Yes, you were very clear. But saying "I want to build a practical system for categorising functions that can be shown to halt or not always halt, but I'm not interested in theory" is kind of like saying, "I want to build a practical warp drive, but I'm not interested in physics."
    - beaconstudios 8y ago
      I'm not interested in trying to encode a proof that addition is commutative. I'm interested in the theory to the point where I'll enjoy (and have been enjoying) learning about the math, but in terms of implementation I just don't want or need to start that low.

lisper 8y ago

> I'm not looking to break through the undecidability barrier That, too, was far from clear. You said you were tackling this problem: > what is the property of a program that makes it undecidable? and I told you: > That is itself an undecidable question! and explained why (at least three times). And AFAICT you still don't get it because you still say you want to: > implement an algorithm that can prove theorems we already know are decidable (well, group functions into the always halts/doesn't always halt/undecidable categories) and that is the problem of automated theorem proving, which is an open research issue, and (provably) always will be. If you want to get a small taste of what you're up against, try proving that this program always halts: f(x:int, y:int) = ( x+y == y+x ? halt : loop ) In other words, try proving the commutative law of addition. If you get that, try to prove that this lambda-calculus expression (λ (n f) (n (λ (c i) (i (c (λ (f x) (i f (f x))))))(λ x f) (λ x x))) computes a factorial expressed as a Church numeral. (See http://www.flownet.com/ron/lambda-calculus.html http://www.flownet.com/ron/lambda-calculus.html for some hints.) And that's just what you get from elementary arithmetic. If you really want to blow your mind, look at: http://www.mrob.com/pub/math/largenum.html http://www.mrob.com/pub/math/largenum.html and the associated software: http://www.mrob.com/pub/perl/hypercalc.html http://www.mrob.com/pub/perl/hypercalc.html Once you get to infinity you are only just getting started: https://johncarlosbaez.wordpress.com/2016/06/29/large-countable-ordinals-part-1/ https://johncarlosbaez.wordpress.com/2016/06/29/large-counta... And even all that is just what you get from discrete math! Then there's calculus, topology, algebraic varieties (of which elliptic curves are one example, and even that is a whole field of study). And even here we've not even begun to scratch the surface of what is possible. The world of math is (provably!) richer than you -- or anyone -- can possibly imagine! That's what "undecidable" means. Your only reasonable hope of making any kind of non-trivial progress is to focus on one domain, and then use the constraints imposed by the properties of that domain to shrink the problem down to something potentially manageable.

beaconstudios 8y ago
See, I'm not an academic - proving that addition is commutative is not in scope for what I'm wanting to do. It is not a big leap for me to make that an axiom in my system, I'm almost entirely disinterested in trying to innovate in the pure theory of foundational mathematics. I find the theory itself extremely interesting but that's just not my path. I thought I was clear about what I was wanting to build - a practical system for categorising functions that can be shown to halt or not always halt, lumping everything else into a third category. Academia and pure maths just isn't for me, this is so I can build a language with minimal bugs.
- lisper 8y ago
  Yes, you were very clear. But saying "I want to build a practical system for categorising functions that can be shown to halt or not always halt, but I'm not interested in theory" is kind of like saying, "I want to build a practical warp drive, but I'm not interested in physics."
  - beaconstudios 8y ago
    I'm not interested in trying to encode a proof that addition is commutative. I'm interested in the theory to the point where I'll enjoy (and have been enjoying) learning about the math, but in terms of implementation I just don't want or need to start that low.