4 ms·

I think it was the lack of a stronger Type-theoretic approach to classifying the 'world' of computation. This categorical 'program morphism' is ill-defined when

I think it was the lack of a stronger Type-theoretic approach to classifying the 'world' of computation. This categorical 'program morphism' is ill-defined when taken back to the world of computation (is it supposed to represent sequential execution?). It is also clear that every object within the closed category will have an equivalent morphism and vice-versa (and thanks to the nature of Type Theory, it will also be infinite and still allow for crazy paradoxes like the entire Category being an object of itself). I guess it's the categorical approach to Type Theory? Some other things as well. But this is what I collected after a quick review. :) EDIT: Oh yeah I also find this statement abhorrent: >While a Turing machine can be seen as an idealized, simplified model of computer hardware, the lambda calculus is more like a simple model of software. It should be removed :/

tel 12y ago
W.r.t. to the comparison of Turing Machines and Lambda Calculus, I don't find that a terrible first approximation of the difference of feeling between the two. I'd like to know why you consider it abhorrent—I'd merely call it gestural at best. As far as the first concern I think Baez and Stay were pretty explicit that they're only talking about typed lambda theories and typed linear lambda theories. You can give computation semantics by picking canonical forms of equivalence classes of lambda terms. I'm not sure what the concern is with every object having a morphism—that's true axiomatically of categories due to the id arrows. Is that what you mean? I don't think there's any category which is its own object, but you could see an embedding of linear lambda calculus inside itself since one of those morphisms will be an interpreter. I tend to find this paper really illuminating and instructive, though I'd freely admit that the computation section is not a robust theory of practical computation but instead an exploration of lambda theories.
- StandardFuture 12y ago
  >I'd like to know why you consider it abhorrent 1. I am a Turing fan-boy. 2. I am also a big advocate of the fact that Software IS hardware. And in reality, all computation is software ('hardware' is merely the materials engineering that implements the computational 'logic' e.g. Electrical Engineering for modern-day computers). Classifying a Turing Machine as a 'hardware' abstraction is just so not true. It's an Abstract Computational Machine -- it abstracts the concept of computation (not the fact that it uses a Tape, etc.) and as I said earlier: computation IS software. >I'm not sure what the concern is with every object having a morphism Every program is a function type, and every type is an object. Thus, (type-theoretically at least) every object within the category is also a morphism and vice-versa. Considering Turing Completeness, we can create any program and thus any type from other types (it itself being a type). Thus, the Category can be achieved as a whole as a 'program-type (function type)' since everything within the category is a type itself. This creates strange paradoxes, where the category (and all sub-categories and functors between them) are inside the category itself. (Side-thought: I wonder though if you could address decision problems with this craziness.) >typed linear lambda theories Symmetric Monoidal Categories give rise to Linear Type Theories. 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). >I tend to find this paper really illuminating and instructive Me too. :) >but instead an exploration of lambda theories. hehe, I'm not a fan of Lambda Theories (but please excuse my bias). EDIT: An explanation for the downvote would be appreciated. Thanks. :)
  - deleted 12y ago
    [deleted]
  - tel 12y ago
    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. Edit: Note, I wasn't the downvoter.
    - StandardFuture 12y ago
      >compare TM and LC 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

tel 12y ago

W.r.t. to the comparison of Turing Machines and Lambda Calculus, I don't find that a terrible first approximation of the difference of feeling between the two. I'd like to know why you consider it abhorrent—I'd merely call it gestural at best. As far as the first concern I think Baez and Stay were pretty explicit that they're only talking about typed lambda theories and typed linear lambda theories. You can give computation semantics by picking canonical forms of equivalence classes of lambda terms. I'm not sure what the concern is with every object having a morphism—that's true axiomatically of categories due to the id arrows. Is that what you mean? I don't think there's any category which is its own object, but you could see an embedding of linear lambda calculus inside itself since one of those morphisms will be an interpreter. I tend to find this paper really illuminating and instructive, though I'd freely admit that the computation section is not a robust theory of practical computation but instead an exploration of lambda theories.

StandardFuture 12y ago
>I'd like to know why you consider it abhorrent 1. I am a Turing fan-boy. 2. I am also a big advocate of the fact that Software IS hardware. And in reality, all computation is software ('hardware' is merely the materials engineering that implements the computational 'logic' e.g. Electrical Engineering for modern-day computers). Classifying a Turing Machine as a 'hardware' abstraction is just so not true. It's an Abstract Computational Machine -- it abstracts the concept of computation (not the fact that it uses a Tape, etc.) and as I said earlier: computation IS software. >I'm not sure what the concern is with every object having a morphism Every program is a function type, and every type is an object. Thus, (type-theoretically at least) every object within the category is also a morphism and vice-versa. Considering Turing Completeness, we can create any program and thus any type from other types (it itself being a type). Thus, the Category can be achieved as a whole as a 'program-type (function type)' since everything within the category is a type itself. This creates strange paradoxes, where the category (and all sub-categories and functors between them) are inside the category itself. (Side-thought: I wonder though if you could address decision problems with this craziness.) >typed linear lambda theories Symmetric Monoidal Categories give rise to Linear Type Theories. 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). >I tend to find this paper really illuminating and instructive Me too. :) >but instead an exploration of lambda theories. hehe, I'm not a fan of Lambda Theories (but please excuse my bias). EDIT: An explanation for the downvote would be appreciated. Thanks. :)
- deleted 12y ago
  [deleted]
- tel 12y ago
  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. Edit: Note, I wasn't the downvoter.
  - StandardFuture 12y ago
    >compare TM and LC 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