My Math Forum  

Go Back   My Math Forum > Math Forums > Math

Math General Math Forum - For general math related discussion and news


Thanks Tree3Thanks
Reply
 
LinkBack Thread Tools Display Modes
June 5th, 2017, 03:24 PM   #1
Newbie
 
Joined: Mar 2016
From: Alabama

Posts: 18
Thanks: 0

Foundations questions

1. Would an axiomatic theory of algorithms that transform any given input set to any arbitrary output set ("arbitrary" in the sense of "need not satisfy any particular criteria", not "arrived at by a nondeterministic process") be equivalent to a theory of universal computation?

2. In what way is a foundational theory of computation different from a foundational theory of mathematics? In particular, is either reducible to the other by reasonable standards of judgment?
zambod is offline  
 
June 5th, 2017, 03:40 PM   #2
Senior Member
 
Joined: Aug 2012

Posts: 1,510
Thanks: 364

Quote:
Originally Posted by zambod View Post
1. Would an axiomatic theory of algorithms that transform any given input set to any arbitrary output set ("arbitrary" in the sense of "need not satisfy any particular criteria", not "arrived at by a nondeterministic process") be equivalent to a theory of universal computation?
Since most functions (from $\mathbb N \to \mathbb N$, say) are not computable, most of these functions have no algorithms and go far beyond any possible theory of computation, at least as we currently understand the word.

Quote:
Originally Posted by zambod View Post
2. In what way is a foundational theory of computation different from a foundational theory of mathematics?
Computation is essentially constructive mathematics. However there are many flavors of constructive math so this statement should not be taken too literally.

Quote:
Originally Posted by zambod View Post
In particular, is either reducible to the other by reasonable standards of judgment?
If you start with standard math (axioms of ZFC set theory for example) and throw out everything that's not computable via a Turing machine, you get computability theory. Although to be fair, computer scientists do sometimes employ ideas that go beyond Turing machines, such as oracles.
Thanks from zambod

Last edited by Maschke; June 5th, 2017 at 03:48 PM.
Maschke is offline  
June 5th, 2017, 04:28 PM   #3
Newbie
 
Joined: Mar 2016
From: Alabama

Posts: 18
Thanks: 0

Quote:
Originally Posted by Maschke View Post
Since most functions (from $\mathbb N \to \mathbb N$, say) are not computable, most of these functions have no algorithms and go far beyond any possible theory of computation, at least as we currently understand the word.
Why is halting so central to our definition of algorithms? Is it because it's harder to enumerate the properties of procedures that don't halt? Where would a semantic approach like Computability logic fit into these categories? (To be more specific: It's probably a yet-to-be successful attempt at creating a "logic" corresponding to games in general. There are incomplete attempts at creating game semantics corresponding to intuitionistic type theory, but as far as I know, any such semantics is distinct from the underlying type theory. But then what do you get if you start from games and try to axiomatize them? That's the source of my confusion. IIRC, with its focus on "winning", Computability logic still falls within the universe of halting functions.)

Last edited by zambod; June 5th, 2017 at 04:47 PM.
zambod is offline  
June 5th, 2017, 04:48 PM   #4
Senior Member
 
Joined: Aug 2012

Posts: 1,510
Thanks: 364

Quote:
Originally Posted by zambod View Post
Why is halting so central to our definition of algorithms? Is it because it's harder to enumerate the properties of procedures that don't halt? Where would a semantic approach like Computability logic fit into these categories?
That link appears to be the personal project of one individual. I didn't read enough to call it cranky but his comments on syntax versus semantics seems to me to diverge from their commonly accepted usage. I really have no idea what it's about.

As far as the halting problem, its importance is that it's the standard example of an easily stated problem that can not possibly be solved by an algorithm.

Your question, "why is halting central to the definition of algorithms," does not seem to make sense. Halting has nothing to do with the definition of algorithms. Once you define an algorithm, the halting problem pops up as a problem that can't be solved by an algorithm.

Can you say more about where your questions are coming from? Are you taking a class, are you the author of the paper you linked, are you pushing an agenda, trying to learn CS? I must say I was put off by the linked paper since in its very first paragraph it veers off into its own world.

If nothing else (and there's plenty more else) take the statement, "... classical logic is a systematic tool for telling what is true." Since classical logic can never tell us what is true, what am I supposed to make of the rest of the paper? Are there translation errors involved that make this paper seem crankier than it is?
Thanks from zambod

Last edited by Maschke; June 5th, 2017 at 04:52 PM.
Maschke is offline  
June 5th, 2017, 05:04 PM   #5
Senior Member
 
Joined: Aug 2012

Posts: 1,510
Thanks: 364

Are you the author of the paper?

There is an article on CoL on Wiki

https://en.wikipedia.org/wiki/Computability_logic

It reads like an outline of the paper. Most of the references are to works by the same author. In the Talk page (click on Talk at the top of the Wiki page) I found the following comment:

This entry strikes me as self-advertising by Mr. Japaridze. There are quite a few "computational logics" like this one; an expert should decide whether Mr Japaridze's theory is such a break-through as to deserve a single entry to itself.

This is my impression too. The author has a Ph.D. and is serious about his research project, but now he seems to have written his own Wiki page (against Wiki rules) to promote his ideas. And someone else on the Talk page noted, as I did, that calling classical logic a theory of truth is flat out wrong.

If you're the author, I'm in no position to debate your ideas. But if you're just someone trying to learn computability theory, I'd stay stick to the standard sources and don't worry too much about CoL. My two cents on that.
Maschke is offline  
June 5th, 2017, 05:10 PM   #6
Newbie
 
Joined: Mar 2016
From: Alabama

Posts: 18
Thanks: 0

Quote:
Originally Posted by Maschke View Post
Your question, "why is halting central to the definition of algorithms," does not seem to make sense. Halting has nothing to do with the definition of algorithms. Once you define an algorithm, the halting problem pops up as a problem that can't be solved by an algorithm.
Are you sure about this? I'm pretty sure that a computable function corresponds to a recursive language, and recursive languages require their Turing machines to halt in all cases.

Quote:
Originally Posted by Maschke View Post
Can you say more about where your questions are coming from?
I'm a student. It's possible I gave the paper too much credit because it comes from a scholarly source.
zambod is offline  
June 5th, 2017, 05:19 PM   #7
Senior Member
 
Joined: Aug 2012

Posts: 1,510
Thanks: 364

Quote:
Originally Posted by zambod View Post
Are you sure about this? I'm pretty sure that a computable function corresponds to a recursive language, and recursive languages require their Turing machines to halt in all cases.
If you don't require TMs to halt you get a radically different definition of computability. I'm not familiar enough with CS to say if halting is regarded as too strong a constraint, but I don't think anyone is making that claim.

Quote:
Originally Posted by zambod View Post
I'm a student. It's possible I gave the paper too much credit because it comes from a scholarly source.
I'm sure the paper is valid but it doesn't seem to bear on anything elementary. If he's trying to develop a logic for computable game theory that's way beyond my expertise.

Last edited by Maschke; June 5th, 2017 at 05:22 PM.
Maschke is offline  
June 6th, 2017, 04:58 AM   #8
Newbie
 
Joined: Mar 2016
From: Alabama

Posts: 18
Thanks: 0

Quote:
Originally Posted by Maschke View Post
If you don't require TMs to halt you get a radically different definition of computability. I'm not familiar enough with CS to say if halting is regarded as too strong a constraint, but I don't think anyone is making that claim.
The halting condition is logically related to the requirement in constructive mathematics that you must produce an object. A procedure that may not halt may not "produce an object". AIUI, because there is no upper limit on the length of a natural number, a procedure that generates literally "any natural number" is not guaranteed to halt. This is why a natural number can only be checked/accepted by a TM. But the requirement that an algorithm must halt is externally imposed on imperative languages, and TMs are imperative in their operation.

Mathematically, is there any reason to think we can't find structural regularities in the execution of a non-halting procedure? Theoretically, in the Hoare logic model of imperative languages, "termination must be proved separately" as Wikipedia puts it: https://en.wikipedia.org/wiki/Hoare_logic In practice, loops that are not guaranteed to terminate have real world applications in programs that are supposed to run until the user quits, to give one example. Are such programs not "algorithms" if we can't prove that the user will quit?

These are my grounds for thinking that computer science can be more classical than constructive if we put effort into discovering such a theory.

Quote:
Originally Posted by Maschke View Post
I'm sure the paper is valid but it doesn't seem to bear on anything elementary. If he's trying to develop a logic for computable game theory that's way beyond my expertise.
How can it not have a bearing on these questions? The project is meant to investigate the foundations of computation. My original question was, "In what category would such an approach fit?"

Trying to answer this question runs into a couple of snags. To be brutally honest, at its current stage of development, it looks like a bunch of completely unrelated minilogics to me. For comparison, this is what a successful 'Game-theoretic Model of Computation' looks like: https://arxiv.org/abs/1702.05073

Can you haul scrap metal from a junkyard onto your lawn and call it a "future car"? It's not easy to enumerate the properties of objects that we're not sure can "exist", as it were, in principle. That's the reason I gave for why "algorithms" are required to halt in all cases, but classical mathematics is on surer footing than some unknown "Computability logic" that may or may not exist in some unknown corner in the space of consistent concepts. Since classical mathematics analyzes functions that are not guaranteed to halt, it follows that the reason I gave falls short of being a sufficient deterrent.

Last edited by zambod; June 6th, 2017 at 05:53 AM.
zambod is offline  
June 6th, 2017, 01:51 PM   #9
Senior Member
 
Joined: Aug 2012

Posts: 1,510
Thanks: 364

I wish I could respond to this at the level of knowledge it requires. I have only tangential knowledge of computer science and not all that much math either. You might consider clarifying your question down to something specific and answerable, and posting it on cs.stackexchange or else any of the Reddit groups for CS, algorithms, etc.

That said, I found your post interesting and I have some comments that might be of interest.


Quote:
Originally Posted by zambod View Post
The halting condition is logically related to the requirement in constructive mathematics that you must produce an object.
Yes, I noticed this in something I read somewhere. If $P$ is a unary predicate then the expression $\exists x P(x)$ asserts the existence of something but does not provide a recipe for cooking one up. Constructivists are people who are bothered by this.

On the other hand, computation is inherently constructive. It's exactly the study of everything we can construct using algorithms.

So I am arguing that the link between computation and constructive math is more circumstantial than philosophical. In other words computation just happens to be about recipes, and constructivists like recipes. But I think the study of computation is itself agnostic to the philosophy. If computation turned out to involve nonconstructive elements then the computer scientists would just do that. They wouldn't be bothered by using nonconstructive math if that's what they needed to do to study computation. Whereas the constructivists would be annoyed.

Does that make sense?

I have a datapoint to support this opinion later.

Quote:
Originally Posted by zambod View Post
A procedure that may not halt may not "produce an object". AIUI, because there is no upper limit on the length of a natural number, a procedure that generates literally "any natural number" is not guaranteed to halt. This is why a natural number can only be checked/accepted by a TM. But the requirement that an algorithm must halt is externally imposed on imperative languages, and TMs are imperative in their operation.
Yes, I think I understand that. That's why for example determining if a floating point number is zero is not computable. Because in an idealized (infinite memory) implementation, no matter how many 0's you see, you can never be sure whether the next digit will be 1. So floating point numbers are conceptually broken. You can't map the mathematical (nonconstructive) real numbers onto computations.

Quote:
Originally Posted by zambod View Post
Mathematically, is there any reason to think we can't find structural regularities in the execution of a non-halting procedure?
Ah ... non-halting procedure. Let me think about that a little.

First, I was going to say that if we forget procedures and talk about bitstrings instead, then there are uncountably many bitstrings and only countably many procedures so almost all bitstrings have no "structural regularities." So that's a blunt force way to look at the problem.

But it occurs to me that you're talking about something more subtle. Procedures that don't halt. I don't know anything about those. So maybe this is something people study.

I do know that there is a concept in math called "definable but not computable." A number is computable if there is an algorithm that cranks out its decimal (or binary) digits. A number is definable if it can be uniquely characterized in the language of first-order Peano arithmetic (or some other system, which may give you a different notion of definability).

It's not hard to whip up a real number that is definable but not computable. One such is Chaitin's $\Omega$. https://en.wikipedia.org/wiki/Chaitin%27s_constant

This number is essentially a bitstring where the n-th bit tells you whether or not the n-th Turing machine (in some particular encoding) halts. This number can not be computable else we'd solve the halting problem. But it's perfectly well definable, I just defined it. (Exercise for the reader to figure out how what I said makes it "definable in first-order Peano arithmetic." That's beyond the limits of my knowlege).

Now what's interesting is that Chaitin used his ideas to prove Gödel's incompleteness theorems in purely information-theoretic terms. So we're actually in the realm of Gödelean incompleteness here.

And here is something not too well known. Say you have an axiom system for arithmetic (theory of the natural numbers). We know it's incomplete, so there's some statement we can neither prove nor disprove. So we pick a truth value arbitrarily and add that as a new axiom. Now we have a NEW axiom system (the original one plus the independent statement or its negation). But this new system must ALSO be incomplete ... so we can add another axiom ...

You can see that we are going to get an infinite hierarchy of axiom system that kind of branch out in all directions. And do you who studied this? None other than Turing. His doctoral dissertation was about "Ordinal models of computation," in which he used the mathematical theory of the ordinal numbers to keep track of the structures you get when you keep extending axiom systems.

https://en.wikipedia.org/wiki/System...ed_on_Ordinals

This is related to oracles. You assume you have a magic box that computes something noncomputable, and you see what you get.

So Gödel, Turing, and Chaitin are all over this mysterious realm of extensions beyond what's computable. And I believe this is what you are talking about.

Tell me if anything I've written is on target.



Quote:
Originally Posted by zambod View Post
Theoretically, in the Hoare logic model of imperative languages, "termination must be proved separately" as Wikipedia puts it:
I read that section of the page and I think you read more into that quote than I did. But I'm really unfamiliar with formal approaches to computation although I've heard Hoare's name.



Quote:
Originally Posted by zambod View Post
https://en.wikipedia.org/wiki/Hoare_logic In practice, loops that are not guaranteed to terminate have real world applications in programs that are supposed to run until the user quits, to give one example. Are such programs not "algorithms" if we can't prove that the user will quit?
I have the same question myself. A web browser obviously does not halt. It has no way of knowing whether the user will click on something in five minutes or whether the world has ended and there will be no more clicks.

So is a web browser not a computation in the sense of computer science? In which case, what is it?

It's sort of like in math, if you define "proof" the way they do in logic, no working mathematician has ever seen a proof. If you define program as a computer scientist does, once you get beyond "hello world" no working programmer has ever seen a program! Small exaggeration but you get the idea.

I have wondered about this for a long time.






Quote:
Originally Posted by zambod View Post
These are my grounds for thinking that computer science can be more classical than constructive if we put effort into discovering such a theory.
I wonder if the business about oracles and such is a step in that direction. We do go beyond computability by allowing one new noncomputable thing at a time.

But in math, we have a LOT of uncomputable things. Uncountably many. Too many to be accounted for in ANY possible formal system of symbol manipulation. Those kinds of systems are inherently countable.

So there's three levels:

* Computable.

* Definable but not computable. Extending axiom systems one new statement at a time. Chaitin's ideas. Oracles.

* Full mathematical ontology. Uncountably many real numbers, existence without recipes.


Quote:
Originally Posted by zambod View Post
How can it not have a bearing on these questions?
The CoL thing? I confess that all I got out of it was that it is advanced and esoteric, not really bearing on the things I'm talking about at all. But I could be wrong.

On a pragmatic basis I think you'd be much better off reading Chaitin (who writes pretty clearly) than this other guy who seems to be working in a very small area consisting mostly of himself and a couple of others. Just my impression.

Quote:
Originally Posted by zambod View Post
The project is meant to investigate the foundations of computation. My original question was, "In what category would such an approach fit?"
He seems to be doing advanced research into an obscure area. Even if he's interested in "foundations of computing" his work is too specialized for what you're after. In my opinion of course.

Quote:
Originally Posted by zambod View Post
Trying to answer this question runs into a couple of snags. To be brutally honest, at its current stage of development, it looks like a bunch of completely unrelated minilogics to me. For comparison, this is what a successful 'Game-theoretic Model of Computation' looks like: https://arxiv.org/abs/1702.05073
I think you are trying to run before you can walk. Am I wrong?

Quote:
Originally Posted by zambod View Post
Can you haul scrap metal from a junkyard onto your lawn and call it a "future car"?
Of course. You can look at a rock and see the sculpture inside. Is this some kind of Zen koan kind of question?

Here's a lighthearted philosophical question. If people come by and take parts off the old car on my lawn, one piece at a time, and put them in their cars; and eventually every single part of my old car is now driving around in thousands of different cars; can we say that my car is still on the road?

Quote:
Originally Posted by zambod View Post
It's not easy to enumerate the properties of objects that we're not sure can "exist", as it were, in principle.
Are you talking about recipes? In math we can well-order the real numbers. We don't require there to be an articulable method. Again if you are bothered by this that's fine, but in math you just "get used to it."

Am I understanding you right? What things exist in principle, maybe I lost your meaning here.

Quote:
Originally Posted by zambod View Post
That's the reason I gave for why "algorithms" are required to halt in all cases, but classical mathematics is on surer footing than some unknown "Computability logic" that may or may not exist in some unknown corner in the space of consistent concepts. Since classical mathematics analyzes functions that are not guaranteed to halt, it follows that the reason I gave falls short of being a sufficient deterrent.
I sort of lost the thread of this paragraph. Algorithms are not required to halt. Some do and some don't. Deterrent to what? Sorry I couldn't parse most of this.

Last edited by Maschke; June 6th, 2017 at 02:11 PM.
Maschke is offline  
June 8th, 2017, 10:33 AM   #10
Newbie
 
Joined: Mar 2016
From: Alabama

Posts: 18
Thanks: 0

I've been trying to think about why you find game semantics so exotic when researchers working on it intend it to be a more intuitive model for computation than Turing Machines. Have you studied programming computable functions (PCF), Martin Lof's type theory, linear logic and the early literature on game semantics? The first three are each a set of rules that can be listed on a single page. You can find basic texts on these subjects by Googling: <subject name> pdf
zambod is offline  
Reply

  My Math Forum > Math Forums > Math

Tags
foundations, questions



Thread Tools
Display Modes


Similar Threads
Thread Thread Starter Forum Replies Last Post
Need recommendations for a good foundations of mathematics b vindy Math Books 1 February 22nd, 2014 08:07 AM
Calculus Foundations (Leibniz and Berkeley) bt359 Calculus 1 November 15th, 2013 11:39 AM
Foundations of Geometry carl1234 Math Books 3 February 21st, 2010 01:44 PM
Foundations of Mathematics CRGreathouse Applied Math 10 July 26th, 2008 08:26 PM





Copyright © 2017 My Math Forum. All rights reserved.