Re: domains for typed lambda calculi

Dnia 04-05-2008 o 20:02:27 JohnF <john@xxxxxxxxxxxxxxxxxxxxxxxxxxxx> napisał(a):

Thanks for the recommendations, Michal, which I'll look at soon.
However, your instinct is right that I was actually hoping for
models based on domain equations, like D=[D-->D] for the untyped
lambda calculus. Can anything like that be constructed?
Any references along those lines?

Of course, there are no non-degenerated set-theoretic reflective domains (in any set theory there can be no injection \Omega^D -> D, where \Omega is the subobject classifier; classically, since \Omega = {0, 1}, this means that D \= D^D unless |D| < 2). However, you may either a) take into consideration non-standard exponents (for example, take the category of subsets of natural nubers and partially recursive functions; clearly, N is isomorphic to N^N); b) brake free from the bastile of the standard set theory, and move to a more appropriate (constructive) universe (for example Hyland's effective topos); or both - because the Yoneda Embedding preserves products and exponents, it suffices to construct a relfexive domain (see Lambek's C-monids - ,,Introduction to Higher Order Categorical Logic'' by Lambek and Scott) in any catgory, and than inject it via Yoneda into a topos, obtaining a set theoretic model.


mp
.