Regardless of your belief about the relationship between software and hardware, I think it's reasonable to compare TM and LC by considering TM as "concrete" with its notion of the tape and the algorithm and LC as "abstract" with its notion of reduction and equivalences.
Every program (for a suitable definition of program) is a morphism in a category with objects as types. The types themselves are not (programmatic) objects at all—they're merely the "objects" of the category. The arrows from 1 to a type are the values of that type, though. As stated, Completeness would allow you to embed an interpreter which means some of those arrows ought to look a bit like `(a -> b) -> (a -> b)`, the simplest of which being the `id` arrow on `(a -> b)`. That said, not all theories of typed lambda calculus are Complete.
There's nothing that says a Category has to be well-founded, either, for that matter. If you use set comprehension to deal with the components of your category then you might end up with a Russel's paradox. For mathematics involving "large" categories you use a Universe formalism which lets you dodge those issues for a while.
> However, Braided Monoidal Categories (and especially Monoidal Categories) allow for more. The Rosetta Stone diagram in the conclusion section doesn't restrict the category class (if I remember correctly).
Yep. And there are many kinds of LC. A lot of interesting work comes out of studying them all and comparing them all.
You can, but Turing already did such in 1937 and showed equivalence of expressiveness. :p
>The types themselves are not (programmatic) objects at all—they're merely the "objects" of the category.
Do you mean 'programmatic' in the computational sense or categorical sense?
Because, I was referring to the fact that every program (morphism) also has an equivalent function type (internal hom). Function types are objects within the Category as well. :)
>If you use set comprehension to deal with the components of your category then you might end up with a Russel's paradox.
It seems that this paper is using a set-theoretic comprehension for the concepts. Although, you could consider 'more powerful' constructions like Universes.
I know a lot has been put into the study of LCs and I have nothing against studying them. I just have a personal preference to use other 'methods' to study computational theory. :p
I think we're just talking around one another. I don't understand how your criticisms are anything besides style, I suppose. If you dislike LC and distrust the mechanics of CT then of course a paper which uses CT to unify LC with math and physics won't float your boat—but it's still perfectly cromulent.
Every program (for a suitable definition of program) is a morphism in a category with objects as types. The types themselves are not (programmatic) objects at all—they're merely the "objects" of the category. The arrows from 1 to a type are the values of that type, though. As stated, Completeness would allow you to embed an interpreter which means some of those arrows ought to look a bit like `(a -> b) -> (a -> b)`, the simplest of which being the `id` arrow on `(a -> b)`. That said, not all theories of typed lambda calculus are Complete.
There's nothing that says a Category has to be well-founded, either, for that matter. If you use set comprehension to deal with the components of your category then you might end up with a Russel's paradox. For mathematics involving "large" categories you use a Universe formalism which lets you dodge those issues for a while.
> However, Braided Monoidal Categories (and especially Monoidal Categories) allow for more. The Rosetta Stone diagram in the conclusion section doesn't restrict the category class (if I remember correctly).
Yep. And there are many kinds of LC. A lot of interesting work comes out of studying them all and comparing them all.
Edit: Note, I wasn't the downvoter.