and added pointer to:
I have expanded the first paragraph of the Idea-section, linking it to denotational semantics.
]]>Toby,
Mike mentions (at this blog post by Andrej Bauer) this paper by Aaronson: NP-complete Problems and Physical Reality. Sorta relevant.
]]>Thanks, Toby.
Then I suppose that the specification of the resource bounds is essentially in the choice of what is called “feasible”. Right?
]]>Yes, I wanted to mention Nelson’s hierarchy of feasible numbers, but I’d gone on long enough.
@Mike, see http://mathoverflow.net/q/71386 Although perhaps a realisability style pretopos is better than a topos, since exponentials are suspect.
]]>OK, it's trivial in practice, but we still want to understand it in theory!
I mean, there's a reason that people care whether something is in $P$. But we realize that this says at once too much and too little: something can be practical but not in $P$ (because we're only computing it for a small $n$ where it can be done), and something can be in $P$ but not practical (because $n$, the leading coefficient, or the exponent is large). The former problem I will let live; any problem may be practical for small $n$, and we're usually happy when it is anyway. But the latter problem I would like to fix, by demanding that $n$, the coefficients, and the exponent must exist.
Actually, in practice, it's easy to find real-life problems in $P$ such that the problem is impractical at some $n$ that clearly exist, with the coefficients and the exponent also clearly existing. But there is still some sense that people find that problems in $P$ continue to be practical for a while. So abandon $n$ and look at the coefficients and the exponent.
I think that Edward Nelson's concept of countable, addable, and multiplicable numbers is relevant here. Most ultrafinitists speak simply of feasible numbers (if they don't just speak of numbers and refuse to qualify it at all), but Nelson has a hierarchy of more and more restricted concepts of number. (Since the countable numbers are the largest class and ‘countable’ has other meanings, I prefer to use the word ‘feasible’ for them. Then a number is addable iff its sum with any feasible number is feasible, and a number is multiplicable iff its product with any addable number is addable.) Nelson does not consider exponentiable numbers, since they don't behave as well, but they can be defined.
Then (these are now my definitions, not Nelson's, although he may also have thought of this) a polynomial is feasible if its degree is feasible and so are all of its coefficients; it's addable if its degree is feasible and its coefficients are all addable; it's multiplicable if its degree is addable and its coefficients are all multiplicable; and it's composable if its degree is exponentiable and its coefficients are all multiplicable. Or something like that.
We then get more and more restrictive classes of polynomials, defining more and more practically computable problems, with stronger and stronger closure properties.
]]>Maybe ultrafinitism is the internal language of some topos in which the “natural numbers” exist less and less as one goes out to infinity?
]]>I actually like ultrafinitism as a potential way to formalize […] what is practically computable.
But is there much to be formalized here? It seems fairly trivial: Practically computable is everything that is computable within a given bound of resources, the bound depending on the actual practice. There seems little further to be said in general.
(Maybe ultrafinitism is to mathematics as interpretation of quantum mechanics is to physics. )
]]>True; on one particular machine there may be a hard cutoff (and even that depends on what else that machine is doing), but not in computing as a whole.
I actually like ultrafinitism as a potential way to formalize (if we can formalize ultrafinitism!) what is practically computable. Often people will say that computation problems in $P$ (polynomial-time) are practical, but this is only relative practicality in an infinite limit. If you have a polynomial with a large degree or even a large leading coefficient, then this is immediately impractical; and with any non-constant polynomial, the problem becomes eventually impractical. But if the degree, leading coefficient, and input to the polynomial are restricted to numbers that exist ultrafinitistically, then (perhaps!) we can conclude that the problem is practical.
]]>@Toby, in reality one doesn’t really ’hit a wall’, just a temporary pause until more resources are available. As one needs more space/power, it gets more difficult to get them. Hypothetically I could convince Google to let me use their total computing power, or the owners of that big data centre in Utah. More realistically I could purchase cloud time ’as needed’. There no hard cutoff until we reach total use of planetary resources. And even then…
The important thing as you point out is that proofs with many many symbols are not accepted, not just large numbers.
]]>But ultrafinitists (well, some of them, perhaps not Zeilberger) want to be able to compute freely with natural numbers without having to think that they may suddenly hit a wall. If you're on a machine with finite resources, then at some point you run out of resources, so that $x$ exists but $x + 1$ does not. But ultrafinitism should include an axiom that every natural number has a successor. It just should not include the theorem that $10^{10^10}$ exists.
What makes formalization of ultrafinitism difficult is that non-ultrafinitists will claim that there is a proof that $10^{10^10}$ exists using only the axiom that every natural number has a successor. But ultrafinitists don't accept that that proof exists! So in a way, what's really difficult is not a formalization of ultrafinitism as such but a formalization that is comprehensible to a non-ultrafinitist.
]]>Okay, good.
So that’s the sought-after formalization of ultrafinitism then: non-computability of sufficiently large canonical forms in type theory implemented on a machine with finite resources.
Seems to be simple enough.(!?)
]]>@Urs - I completely agree, and this agrees with what I see in Zeilberger’s work. One can say something like
$2^googol + 2^{googol^googol}$but evaluating this will never happen. We are perfectly happy to say this is equal to $2^{googol^googol} + 2^googol$, but the statement is purely formal, like saying ’given a measurable cardinal…’ or ’given a proper class of Woodin cardinals…’
]]>In discussion of formalization (or lack thereof) of ultrafinitism, by David Roberts on g+ here I am wondering if the concept of numerals is not a good way to capture what is at issue here.
Given any installation of Coq, the system will confirm within a tiny amount of time that the term
10^10^10^10^10^10^10^10 : Nat
is well typed. On the other hand, bringing that term to canonical numeral form will fail to terminate on all available hardware, due to running out of (space and/or time) resources. I suppose.
So in this sense the term in question here “exists” only in one of two possible senses. It exists as a term, but, within the given installation, not as a term of canonical form. This might be just the formalization of what is at stake in ultrafinitism. (?)
]]>I’m not sure whether there was any disagreement or confusion left over at the end of this discussion, but I just ran across the following quotation from Per Martin-Löf in “An intuitionistic theory of types: predicative part”, 1973:
A closed normal term with type symbol $N$, which obviously must have the form $s(s(...s(0)...))$, is called a numeral.
So I thought I would share it.
]]>Is that similar to your system?
Yes.
]]>Okay, I’m glad we’re all happy with the entry. (-:
I am reminded that the Coq standard library also includes a definition of natural numbers using binary notation rather than unary. Obviously the same ideas would work for base 10 rather than base 2. Is that similar to your system?
]]>You have to follow me on Facebook to know that kind of thing, I guess.
]]>For those who knew me eight years ago and wonder why they never heard of this before: she is adopted, and actually even that process is not completed yet.
Well, well, well! I had no idea.
]]>Looks fine!
Ditto!
]]>I’ve edited the page numeral to discuss both the informal and formal meanings; see what you think.
Looks fine!
]]>I have thought about making a kind of computer-algebra system that does calculations in the way that people are taught in schools. (This is the sort of thing that I think about when trying to teach people how to do them.) Since we need to make contact with the notation used by humans, the numerical part would use a system extending that in my comment #14. (Not the systems from #15, which are uglier; so I would just have sped-up algorithms proved to give results equivalent to the slow definitions.)
]]>As jcmckeown's post suggests, there's also a formal system in which $s(s(s(s(s(s(s(s(s(s(s(s(0)))))))))))))))))$ beta-reduces to $13$. This has the same language as above, but now the operation written as concatenation is primitive while $s$ is defined as $s + 1$. Also, $1$ through $9$ are primitive, and $+$ is defined directly in terms of the primitive operations rather than (which would be circular) in terms of $s$. (A similar remark applies to $\cdot$, although this doesn't appear in the beta-reduction of $s(s(s(s(s(s(s(s(s(s(s(s(0)))))))))))))))))$.) The full definition of $+$ is rather complicated, and there are many noncanonical terms that don't beta-reduce to any canonical ones, (such as $2(36)$, which is only provably equal to $56$), so this system is not as nice as the previous one.
Another system in which $s(s(s(s(s(s(s(s(s(s(s(s(0)))))))))))))))))$ beta-reduces to $13$ would have unary operators $0$ through $9$, written as postpositions, and an invisible constant. The recursive definition of $+$ is much simpler now, such that I almost don't mind writing it down (but watch out for the hard-to-spot invisible constants):
$\array{ {} + {} \coloneqq {} ;\\ {} + b0 \coloneqq b0 ;\\ \vdots\\ {} + b9 \coloneqq b9 ;\\ a0 + {} \coloneqq a0 ;\\ a0 + b0 \coloneqq (a + b)0 ;\\ a0 + b1 \coloneqq (a + b)1 ;\\ \vdots\\ a0 + b9 \coloneqq (a + b)9 ;\\ a1 + {} \coloneqq a1 ;\\ a1 + b0 \coloneqq (a + b)1 ;\\ a1 + b1 \coloneqq (a + b)2 ;\\ \vdots\\ a1 + b8 \coloneqq (a + b)9 ;\\ a1 + b9 \coloneqq (a + b + 1)0 ;\\ \vdots\\\vdots\\\vdots\\ a9 + b9 \coloneqq (a + b + 1)8 .}$And now I can essentially show the reduction:
$\array{ s(s(s(s(s(s(s(s(s(s(s(s(0))))))))))))))))) & \rightsquigarrow s(s(s(s(s(s(s(s(s(s(s(0))))))))))))))))) + 1 \\ & \rightsquigarrow s(s(s(s(s(s(s(s(s(s(0))))))))))))))))) + 1 + 1 \\ & \cdots \\ & 0 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 \\ & \rightsquigarrow ({} + {})1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 \\ & \rightsquigarrow 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 \\ & \rightsquigarrow ({} + {})2 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 \\ & \rightsquigarrow 2 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 \\ & \cdots \\ & \rightsquigarrow 9 + 1 + 1 + 1 + 1 \\ & \rightsquigarrow ({} + 1)0 + 1 + 1 + 1 \\ & \rightsquigarrow 11 + 1 + 1 \\ & \rightsquigarrow 12 + 1 \\ & \rightsquigarrow 13 }.$This still has the poor feature that there are unreducible noncanonical terms: $0$, $00$, $000$, etc, all of which are only provably equal (once you put in the appropriate axioms) to the invisible constant, as well as $01$, $005$, $000123$, etc.
This second system is almost one that people actually use, although the one that people actually use is a slightly more complicated one, in which the invisible constant only appears when one of the unary operations $0$ through $9$ is directly applied to it, and even $0$ is never directly applied to it when one of these unary operations is applied to the result. If the recursive definitions of $+$ and $\cdot$ are slightly modified (to versions provably equivalent to mine), then we have a theorem that an expression with this restriction beta-reduces to another expression with this condition, now ending in fully canonical forms. My eight-year-old^{1} is learning this formal system now^{2} in school, so it's not too complicated, even though I don't want to write it all out.
For those who knew me eight years ago and wonder why they never heard of this before: she is adopted, and actually even that process is not completed yet. ↩
Well, they're taking a break to study division before completing the definition of multiplication in this system, but she does know the full definition of addition, in that she can beta-reduce correctly even though she could not write down the definition formally. ↩
What system are you thinking of when you say that ’13’ beta-reduces to the corresponding term built out of 0 and s?
I don't know any such system that people are actually interested in, but it's easy to write down one with this property. The language would consist of constants $0$ through $9$, the unary operation $s$, the binary operations $+$ and $\cdot$ and another binary operation written as concatenation (with precedence ahead of $+$ and $\cdot$ and associating on the left). Put in your axioms for $0$ and $s$ (which don't affect beta-reduction anyway) and the usual recursive definitions for $+$ and $\cdot$ (which do affect beta-reduction). Note that $1$ through $9$ also have standard definitions in terms of $0$ and $s$. So it is left to define the operation written as concatenation; it is defined thus:
${a}{b} \coloneqq s(9) \cdot a + b .$Now observe:
$\array{ 13 & \rightsquigarrow s(9) \cdot 1 + 3 \\ & \rightsquigarrow s(s(8)) \cdot s(0) + s(2) \\ & \rightsquigarrow s(s(s(s(7))) \cdot 0 + s(s(s(7))) + s(1)) \\ & \rightsquigarrow s(s(s(0 + s(s(s(6)))) + s(0))) \\ & \rightsquigarrow s(s(s(s(s(0 + s(s(s(5))))) + 0))) \\ & \rightsquigarrow s(s(s(s(s(s(0 + s(s(s(4))))))))) \\ & \rightsquigarrow s(s(s(s(s(s(s(0 + s(s(s(3)))))))))) \\ & \rightsquigarrow s(s(s(s(s(s(s(s(0 + s(s(s(2))))))))))) \\ & \rightsquigarrow s(s(s(s(s(s(s(s(s(0 + s(s(s(1)))))))))))) \\ & \rightsquigarrow s(s(s(s(s(s(s(s(s(s(0 + s(s(s(0))))))))))))) \\ & \rightsquigarrow s(s(s(s(s(s(s(s(s(s(s(0 + s(s(0))))))))))))) \\ & \rightsquigarrow s(s(s(s(s(s(s(s(s(s(s(s(0 + s(0))))))))))))) \\ & \rightsquigarrow s(s(s(s(s(s(s(s(s(s(s(s(s(0 + 0))))))))))))) \\ & \rightsquigarrow s(s(s(s(s(s(s(s(s(s(s(s(s(0))))))))))))) .}$ ]]>