[pron]

> If you generalize to trees and pick the right alphabet, suddenly every element of your datatype is a well-formed lambda term.

How would you feed trees to the computation? Also, once types are involved, nothing can help you. I admit that untyped LC is somewhat of a borderline case.

> It's also unclear if you're talking about the complexity of type inference or type checking

Doesn't matter in this case. Pick a string representation -- any representation -- and see if it's well-formed. You can include the types and then only type checking would be necessary, or not -- and then it's type inference. Either way, the complexity is significant.

> namely the C abstract machine

That's not a machine model.

> it's undecidable whether a state is meaningful

The same goes for any language and your definition on "meaningful". You can always say that something meaningful is a little finer-grained than the language can express, or the validating the language itself is also undecidable. Got simple types? Only primes are meaningful.

> They just don't have many useful properties compared to more "abstract" approaches, and are mostly used to reason about implementation.

My point is that they're not comparable. A glass of water doesn't have the same useful properties as a blender, yet they're both made of molecules. However, there's an objective difference: a blender consumes far more energy, so of course you can use that energy to do more things.

[tome]

> How would you feed trees to the computation

Um, well the computation (can be set up to) proceeed(s) on algebraic datatypes, so this seems trivially easy.

[pron]

:) You're just pushing the complexity into the validation of the algebraic type.

Look, a typed formalism does extra work of proving the type safety of the input. Checking a proof has a non-negligible complexity. If that cost could be ignored, then I have a computation model that solves NP problems in zero time: it has a type system that requires that the types form a proof certificate for the problem. All (obviously valid) inputs are then trivially reduced to "yes". In fact, you know very well that some type systems are Turing complete. If the complexity of validation is ignored, then those models can compute anything that's computable in zero time.

Types can prove things. The cost of the proof is well known, and is related to the difficulty of the problem. The universe doesn't let computational complexity slide. What, you think that God says, "oh, you clever boy, you chose a typed model so I'll let you have this proof for free!" ?

[tome]

> You're just pushing the complexity into the validation of the algebraic type.

Who says it needs to be validated, any more than your string needs to be validated?

> The universe doesn't let computational complexity slide. What, you think that God says, "oh, you clever boy, you chose a typed model so I'll let you have this proof for free!" ?

You're responding to something completely unrelated to my statement.

To be clear: I wasn't suggesting a typed lambda calculus.

[pron]

A tree is still more complex than strings, because it has rules: one parent per node and no cycles. Those need to be validated. But I have absolutely no problem accepting that it is possible to find an encoding of untyped LC which would bring it very close to a TM encoding. This wouldn't be surprising as LC doesn't do more computational work than TM at the validation step (unlike typed formalisms).

I specifically wrote that untyped LC is a borderline case, and it's unclear where precisely we want to draw the line. What is absoutely clear is that System F and TM are essentially, qualitatively and objectively very different, and when people try to compare them, they often, without noticing, describe two different computational problems, with two different complexities.

[l_dopa]

You're positing some new notion of complexity, without a definition, where lists are somehow fundamentally different than trees. Sorry, but that kind of claim requires more than just just an appeal to intuitions about how they might be implemented on a typical CPU. They're both just initial algebras.

The fact that your grand ideas about machine and language models doesn't apply to the lambda calculus should be a hint. We know how lambda calculus relates to typed languages: it's a degenerate case with a single type. Any differences in the complexity of type-inference or checking are between language models. You can't (without wildly waving your hands) formulate a meaningfully comparable problem for TM states.

[tome]

> A tree is still more complex than strings, because it has rules: one parent per node and no cycles. Those need to be validated.

Hmm, I'm not convinced that this is sufficient to show that strings are simpler.

After all, a string has rules too: a cell in the string is either at the beginning, or the end, or the middle, and it has neighbours left, right or not at all depending on those conditions, and at most one such neighbour in each direction. Even appeal to the physical world doesn't help. If I have a physical piece of DNA, how do I know it hasn't mutated so that two different strands branch off it and it becomes, essentially, a degenerate tree?

I do think that the thrust of your argument is correct but it's not as clear cut (at least not yet) as you seem to be making out.

> What is absoutely clear is that System F and TM are essentially, qualitatively and objectively very different

Absolutely agreed! If they weren't, I'd be happy writing my day-to-day code in Turing Machines.

[pron]

You're talking about the graphical representation of a string. A string is any stream of measurements (over time, if you like).

> If they weren't, I'd be happy writing my day-to-day code in Turing Machines.

And if they weren't, we'd see neurons or DNA using type-theory!