3 ms·
A posetal category has at most one arrow in each homset – i.e. it’s a poset dressed up as a category. A definable function is one that can be defined in the pr
by robinhouston 9y ago
A posetal category has at most one arrow in each homset – i.e. it’s a poset dressed up as a category.
A definable function is one that can be defined in the programming language in question. There's a lot more to definability than Turing machines, when you consider higher types: that is, types whose domain is a function type. John Longley has written on this extensively.
- jordigh 9y agoThanks. Is there something to read that puts all of this together, starting from a common base? I really don't know where to start.
- robinhouston 9y agoI know what you mean about not knowing where to start! I think “all of this” is roughly what theoretical computer scientists call “Theory B”, or at least a large chunk of it, and where to start depends on which specific things you find most interesting. Benjamin Pierce’s _Types and Programming Languages_ is a relatively accessible introduction with an emphasis on types, but of course it’s just an overview of a pretty large research area.