On Two Views of Computation in Computer Science
pressron.wordpress.com
On Two Views of Computation in Computer Science
1–10 of 191 posts
Re: On Two Views of Computation in Computer Science
#2This is an interesting article, but I'm still fairly confused about the notion that is made
>Harper’s attack on the utility of machine models and lack of modularity is tantamount to an architect saying to a chemist, “both of our disciplines concern the arrangement of molecules, yet my discipline is superior, as yours doesn’t even have the modular notion of a room!”
But wouldn't the whole point be that a chemist, seeing the room as nothing less than an abstraction, can also understand the room through their given framework? Much in the same way that, for any computational model, we can think of a TM with an Oracle tape, or some similar IO model, that has the same computational power as any defined language?
I'm afraid that I thought I understood the distinction at first: where those who support CT view computation as a fundamental case (e.g. every other mathematical 'primitive' can be derived from a computation with the appropriate oracles[1]) and and the TOP view which sees mathematical foundations as the main case, and then sees computers as being an abstraction of functions in some sense, such that one can construct a calculus of these functions which constitutes a language.
Did I get this all wrong? I'm afraid I still don't understand the main distinction to be honest. It seems that both parties are going around in circles on exactly the same thing, but assuming different axiomatic systems and showing that each is equivalent to the other.
[1] For example, with no oracles, we receive all of constructive mathematics, etc.
Re: On Two Views of Computation in Computer Science
#3It’s really weird that the Church-Turing thesis, which is ridiculously robust at first order, falls apart so comprehensively at higher type.
A statement like that makes me feel like Neel Krishnaswami does not understand the Church-Turing thesis at all (what does the Church-Turing thesis even mean at a "higher type"), but considering that this person has significant experience in this field, much more than I do, I am just going to assume that it is me who does not understand until I read up on this exactly.
Re: On Two Views of Computation in Computer Science
#4The author contends in the article's abstract that machine models are "self-contained" whereas "language models" (not clearly defined, but meant to encompass at least an untyped lambda calculus) are not. But both can be viewed as a state plus a well-defined set of rewriting rules, so I suspect that the article is struggling to make what is really a distinction without a difference.
Re: On Two Views of Computation in Computer Science
#5The author contends in the article's abstract that machine models are "self-contained" whereas "language models" (not clearly defined, but meant to encompass at least an untyped lambda calculus) are not. But both can be viewed as a state plus a well-defined set of rewriting rules, so I suspect that the article is struggling to make what is really a distinction without a difference.
Author here.
> But both can be viewed as a state plus a well-defined set of rewriting rules, so I suspect that the article is struggling to make what is really a distinction without a difference.
1. I state that the untyped lambda calculus is, indeed, a borderline case, and is a simple rewriting system which, in turn, is a special case of a nondeterministic abstract state machine.
2. That many things are abstract state machines does not mean that the computational complexity required to validate whether what you have is a well-formed description is similar.
3. That complexity difference is absolutely huge -- zero for the machine models vs. exponential to undecidable for the typed language models. It is hardly a struggle to draw the conclusion that the two are objectively completely different classes.
Also, I gave a list of machine and language models. The latter group consists of the process calculi and the lambda calculi.
Re: On Two Views of Computation in Computer Science
#6This is an interesting article, but I'm still fairly confused about the notion that is made >Harper’s attack on the utility of machine models and lack of modularity is tantamount to an architect saying to a chemist, “both of our disciplines concern the arrangement of molecules, yet my discipline is superior, as yours doesn’t even have the modular notion of a room!” But wouldn't the whole point be that a chemist, seei…
You can translate and transform many things to many others. The important question is what is the computational complexity of the transformation? If it is large, then the two things are very different.
As Scott Aaronson once said, waterfalls could be viewed as playing chess, but as the complexity of the translation from the "waterfall language" to a chess language understandable by humans is as great as the complexity of an actual chess-playing program, all the work is done in the translation.
So the question you should be asking is where the complexity is being spent and on what.
Re: On Two Views of Computation in Computer Science
#7It’s really weird that the Church-Turing thesis, which is ridiculously robust at first order, falls apart so comprehensively at higher type. A statement like that makes me feel like Neel Krishnaswami does not understand the Church-Turing thesis at all (what does the Church-Turing thesis even mean at a "higher type"), but considering that this person has significant experience in this field, much more than I do, I am…
The Church-Turing thesis is a statement about which functions of type `nat -> nat` are computable, either in the lambda calculus or using Turing machines. This completely disregards:
(0) Computational complexity. Neither the lambda calculus nor Turing machines were invented to answer questions of computational complexity.
(1) Functions at types other than `nat -> nat`. Curiously enough, programming in the real world is seldom about evaluating functions of type `nat -> nat`.
Re: On Two Views of Computation in Computer Science
#8The author contends in the article's abstract that machine models are "self-contained" whereas "language models" (not clearly defined, but meant to encompass at least an untyped lambda calculus) are not. But both can be viewed as a state plus a well-defined set of rewriting rules, so I suspect that the article is struggling to make what is really a distinction without a difference.
Author here. > But both can be viewed as a state plus a well-defined set of rewriting rules, so I suspect that the article is struggling to make what is really a distinction without a difference. 1. I state that the untyped lambda calculus is, indeed, a borderline case, and is a simple rewriting system which, in turn, is a special case of a nondeterministic abstract state machine. 2. That many things are abstract sta…
Could you encode all untyped lambda calculus expressions by just numbering them and writing the number as the string of bits?
Maybe this enumeration is the "external collaborator" in this case, but it's a very simple one.
Re: On Two Views of Computation in Computer Science
#9Earlier quoted context omitted.
Author here. > But both can be viewed as a state plus a well-defined set of rewriting rules, so I suspect that the article is struggling to make what is really a distinction without a difference. 1. I state that the untyped lambda calculus is, indeed, a borderline case, and is a simple rewriting system which, in turn, is a special case of a nondeterministic abstract state machine. 2. That many things are abstract sta…
Could you encode all untyped lambda calculus expressions by just numbering them and writing the number as the string of bits? Maybe this enumeration is the "external collaborator" in this case, but it's a very simple one.
Inside the lambda calculus, the only thing you can do with a lambda abstraction is apply it.
And one thing you can't do using your numbering scheme (which is basically a Gödel numbering) is establish whether two syntactically different functions are extensionally equal (under some fixed reduction strategy).
Re: On Two Views of Computation in Computer Science
#10It’s really weird that the Church-Turing thesis, which is ridiculously robust at first order, falls apart so comprehensively at higher type. A statement like that makes me feel like Neel Krishnaswami does not understand the Church-Turing thesis at all (what does the Church-Turing thesis even mean at a "higher type"), but considering that this person has significant experience in this field, much more than I do, I am…
The Church-Turing thesis is a statement about which functions of type `nat -> nat` are computable, either in the lambda calculus or using Turing machines. This completely disregards: (0) Computational complexity. Neither the lambda calculus nor Turing machines were invented to answer questions of computational complexity. (1) Functions at types other than `nat -> nat`. Curiously enough, programming in the real world…
Does a type exist such that it cannot be mapped to the set of natural numbers?