On Two Views of Computation in Computer Science • Hacker News Board

Re: On Two Views of Computation in Computer Science

#31

Post by tome » Wed, Aug 31, 2016, 10:37 PM UTC

pron wrote: post #18

catnaroek wrote: post #7

Earlier quoted context omitted.

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…

> 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 is how Krishnaswami frames things. From the TOC perspective, there is no such thing as functions at all. Computations consume and produce strings. Both Church and Turing explain how those strings can encode the natural numbers (there was no talk of types by…

How then do you state the Church-Turing thesis? I note that the Wikipedia page claims that Church and Turing themselves used the word "function":

https://en.wikipedia.org/wiki/Church%E2%80%93Turing_thesis#S...

Re: On Two Views of Computation in Computer Science

#32

Post by catnaroek » Wed, Aug 31, 2016, 11:27 PM UTC

TelmoMenezes wrote: post #25

catnaroek wrote: post #11

Earlier quoted context omitted.

You mean mapped one-to-one? Depends on your model of computation. For example, in the simply typed lambda calculus, equipped with a natural number type, as well as structural recursion on it (but not general recursion), `nat` and `nat -> nat` aren't isomorphic types.

Humm... But the set of Turing Machines is countably infinite, and a nat -> nat function is necessarily representable as a Turing Machine.

Externally, in the metalanguage, you can count syntactically distinct terms, and, of course, the collection of terms that have type `nat -> nat` is countable.

Internally, in the lambda calculus itself, or a model of it, there are two caveats, however:

(0) Nothing guarantees that all internal inhabitants of a type are denotable by external pieces of syntax. For example, most real numbers are undefinable. (There are only countably many formulas over a finite alphabet, but uncountably many real numbers, ergo, most real numbers can't be “pinned down” using a formula. That doesn't prevent them from existing. The situation is exactly the same with a type like `nat -> nat`.)

(1) The right internal notion of equality isn't syntactic equality (which doesn't even make sense, for the reason stated above), but extensional equality.

If all of this sounds too strange, read more about model theory, Gödel's completeness theorem, and the Löwenheim-Skolem theorems.

Re: On Two Views of Computation in Computer Science

#33

Post by catnaroek » Wed, Aug 31, 2016, 11:27 PM UTC

marcosdumay wrote: post #24

catnaroek wrote: post #17

Earlier quoted context omitted.

Computers in the real world pass all their time executing the instructions that programmers give them. (Okay, not true, they pass most of their time waiting for I/O to complete, or simply doing nothing.) If a linguistic abstraction prevents you from giving certain classes of wrong instructions, that's very useful, even if the abstraction has no runtime manifestation.

> If a linguistic abstraction prevents you from giving certain classes of wrong instructions, that's very useful, even if the abstraction has no runtime manifestation. No argument about it. But notice that this applies to programmers, not computers. The article is about two groups talking past each other because of different terminology. When you say that "programming in the real world is seldom about functions of na…

> But notice that this applies to programmers, not computers.

It applies to computers, because it's the computer itself that's preventing you from giving it certain classes of wrong instructions. I'm talking about enforcing things mechanically (type checking), not socially (design patterns, best practices, etc.).

Re: On Two Views of Computation in Computer Science

#34

Post by readams » Wed, Aug 31, 2016, 11:27 PM UTC

I'm not really sure I completely understand where the conflict is here. Even in the "machine model" the church-turing thesis "fails spectacularly" once you start adding in unreasonable things like halting oracles. TM+Halting oracle > TM. It's just that the TM+halting oracle doesn't exist in our universe, even though you can define it mathematically.

When building a language, it's similarly easy to introduce "unreasonable" things that either require huge complexity to translate to the machine representation or might even be completely unrealizable in the real world! Even ignoring higher types, compiling a C++ program requires a potentially unbounded amount of work because templates are a turing-complete functional programming language. As stated in the article, just determining if a C++ program is valid is undecidable!

Nothing stops you from designing these languages, but you can't say that Church-Turing fails until you consider also the systems required to actually execute these languages in the real world. If you can't, then your programming language is perhaps an interesting mathematical abstraction, but just as useful ultimately as that TM+halting oracle model of computation.

Re: On Two Views of Computation in Computer Science

#35

Post by catnaroek » Wed, Aug 31, 2016, 11:33 PM UTC

SilasX wrote: post #21

catnaroek wrote: post #14

Earlier quoted context omitted.

> (1) shouldn't matter if there's some mapping between those types and functions of type `nat -> nat`. That's the thing. In some languages, this mapping doesn't always exist. > AIUI, the CTT is equivalent to saying that anything that can be computed at all (regardless of type signature) can be done via the `nat -> nat` functions representable on some TM. The Church-Turing thesis says absolutely nothing about abstract…

>That's the thing. In some languages, this mapping doesn't always exist. The mapping exists, just not necessarily within the language; the CTT is orthogonal to practical difficulties of massaging the data into a usable input format. (e.g. how to convert a binary tree in to the TM's format and vice versa) >The Church-Turing thesis says absolutely nothing about abstraction barriers your language might enforce, e.g., wh…

> The mapping exists, just not necessarily within the language

In practice, people write their programs in a programming language. Some languages (e.g., C, Java, Lisp) only provide leaky abstractions, so programmers always have access to the internal representation of everything, to the detriment of modularity. But there are languages (e.g., Standard ML) that aren't hobbled in this way.

> Those all speak to the issue of how difficult it is (for e.g. a human) to implement the function, not whether language/computation model can compute it at all.

No. In Standard ML, writing a function that inspects the representation of an abstract type isn't “difficult” - it's literally impossible. If you want to do it, you have to use a different language. The type system enforces the separation of concerns, so that you don't have to rely on your discipline alone.

> If you have a computation for which no TM (or asm, C, etc program) exists that computes it, let us know!

Re-read my sentence. I was talking about the converse: There exist programming languages that don't allow you to do everything the target machine can do.

Re: On Two Views of Computation in Computer Science

#36

Post by [deleted] » Wed, Aug 31, 2016, 11:34 PM UTC

clusmore wrote: post #30

pron wrote: post #6

Earlier quoted context omitted.

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 complexit…

>The important question is what is the computational complexity of the transformation? In my view it makes no sense to use metrics from one model on the other. There is no computational complexity involved in the transformations defined in ToP. This is like measuring the computational complexity of a mathematical proof - it has no complexity, it's delcarative.

[deleted]

Re: On Two Views of Computation in Computer Science

#37

Post by catnaroek » Wed, Aug 31, 2016, 11:45 PM UTC

pron wrote: post #18

catnaroek wrote: post #7

Earlier quoted context omitted.

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…

> 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 is how Krishnaswami frames things. From the TOC perspective, there is no such thing as functions at all. Computations consume and produce strings. Both Church and Turing explain how those strings can encode the natural numbers (there was no talk of types by…

> From the TOC perspective, there is no such thing as functions at all.

I agree with you on this one. What actually exists in computing is procedures, which may or may not compute functions. For instance, even in Haskell, so-called “functions” may call `error` or diverge.

However, it's very useful to treat extensionally equal procedures (considering both their effects and their final results) as equal, even if they're syntactically different. This is the basis for compiler optimizations. And the lambda calculus (suitably extended with effectful computations) is better equipped than any machine model to make this identification.

(OTOH, the lambda calculus is a grossly inadequate foundation for concurrency, which is about communication, rather than computation. The main solution I've seen proposed by proponents of functional languages, namely, abusing callCC to get something like cooperative concurrency, is very, very, very bad.)

> Interpreting a computation as one computing functions on the natural numbers or any other set is an entirely interpretive activity that is external to the computation itself.

In practice, people care about the meaning they ascribe to the symbols with which they compute. We use symbols to denote. A meaningless symbol might as well never have been computed at all.

Re: On Two Views of Computation in Computer Science

#38

Post by simondedalus » Wed, Aug 31, 2016, 11:58 PM UTC

catnaroek wrote: post #35

SilasX wrote: post #21

Earlier quoted context omitted.

>That's the thing. In some languages, this mapping doesn't always exist. The mapping exists, just not necessarily within the language; the CTT is orthogonal to practical difficulties of massaging the data into a usable input format. (e.g. how to convert a binary tree in to the TM's format and vice versa) >The Church-Turing thesis says absolutely nothing about abstraction barriers your language might enforce, e.g., wh…

> The mapping exists, just not necessarily within the language In practice, people write their programs in a programming language. Some languages (e.g., C, Java, Lisp) only provide leaky abstractions, so programmers always have access to the internal representation of everything, to the detriment of modularity. But there are languages (e.g., Standard ML) that aren't hobbled in this way. > Those all speak to the issue…

Whether or not you can map everything in the higher order language to the nat -> nat one is what's at issue, not the reverse.

For an analogy, you can map all the natural numbers to real numbers. This proves just about nothing. That you cannot map all the reals to the naturals proves something very important.

It would be truly bizarre if a useful programming language could express something that computation on bits could not.

Re: On Two Views of Computation in Computer Science

#39

Post by catnaroek » Thu, Sep 01, 2016, 12:19 AM UTC

simondedalus wrote: post #38

catnaroek wrote: post #35

Earlier quoted context omitted.

> The mapping exists, just not necessarily within the language In practice, people write their programs in a programming language. Some languages (e.g., C, Java, Lisp) only provide leaky abstractions, so programmers always have access to the internal representation of everything, to the detriment of modularity. But there are languages (e.g., Standard ML) that aren't hobbled in this way. > Those all speak to the issue…

Whether or not you can map everything in the higher order language to the nat -> nat one is what's at issue, not the reverse. For an analogy, you can map all the natural numbers to real numbers. This proves just about nothing. That you cannot map all the reals to the naturals proves something very important. It would be truly bizarre if a useful programming language could express something that computation on bits co…

> Whether or not you can map everything in the higher order language to the nat -> nat one is what's at issue

If you can't map higher-order constructs to Gödel codes (effectively, numerical representations of syntax), you can't always map them to `nat -> nat`. That's precisely my point.

And, if you could map higher-order constructs to Gödel codes, the higher-order abstractions would be lost - all you need to do to break the abstraction is inspect the syntax. Just like, if you have reflection, type abstraction is lost - all you need to do to break the abstraction is use typecase.

Re: On Two Views of Computation in Computer Science

#40

Post by l_dopa » Thu, Sep 01, 2016, 12:21 AM UTC

pron wrote: post #5

pklausler wrote: post #4

The 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…

Why is the complexity of parsing well-formed states from strings somehow interesting? If you generalize to trees and pick the right alphabet, suddenly every element of your datatype is a well-formed lambda term.

It's also unclear if you're talking about the complexity of type inference or type checking, what annotations you're allowing, etc. Your claims about complexity re: states of typed languages are too hand-wavy to engage with.

And yet there's still a glaring error: for a very popular machine model, namely the C abstract machine, it's undecidable whether a state is meaningful (regardless of how you set up your parsing problem).

So, you have an interesting idea about the difference between machine models and languages but it clearly doesn't hold together. People have been studying the relationship between machine models and languages for quite some time, and it's relatively well understood. Machine models are one of the many ways to give semantics to languages. They just don't have many useful properties compared to more "abstract" approaches, and are mostly used to reason about implementation.