[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
Hi Kalani, Here are my two cents. _|_ (bottom/divergence) is a member of every type, including the "empty" type. The cardinality of the empty type is thus 1, not 0. Also, for the same reason, the cardinality of the Bool type is 3, not 2. -> is the constructor of (lazy/call-by-name) continuous functions (ie, not of all possible mathematical functions). 'Continuous' here is in a domain-theoretic sense, sometimes also called 'Scott-continuity'. The cardinality |A->B| is thus not necessarily |B|^|A|. Noting that A and B contain _|_ as noted above, |A->B| is |B|^|A| in case A and B are 'flat' domains/types. Without much ado, Bool and the empty type are flat. Also, note that -o-> usually denotes the strict/eager/call-by-value version of ->. If, again, A and B are flat, |A-o->B| = |B|^(|A|-1), where |A|-1 is the cardinality of non-bottom elements in A, because -o-> can map _|_ in A only to _|_ in B, not to other elements of B. As such, if I assume you meant eager functions over booleans, |Bool-o->Bool| = 3^2 = 9, not 4 (I believe you can easily figure out these nine functions if you note that a function, in addition to returning true or false, may also diverge/"return" _|_). Similarly, we have |A->_|_| = 1. Regards, -Moez > From: [email protected] > Date: Sat, 4 May 2013 11:49:48 -0400 > To: [email protected] > CC: [email protected] > Subject: Re: [TYPES] [tag] Re: Declarative vs imperative > > [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ] > > > And even in the context of Curry-Howard correspondence, classical logic is > > a legitimate setting to discuss > > languages with control operators, first-class continuations, static > > catch/throw a la Scheme etc. > > I am not an academic or qualified in any way to speak on this, I'm just an > uneducated, small town, country programmer, but on this point you've raised I > wonder if the list could clear up a bit of confusion that I have. > > I'm familiar with thinking of types as sets and logical connectives (type > constructors) as operations on sets. So the type A*B has size |A|*|B|, the > product of the sizes of two sets. A->B has size |B|^|A| and this works out > well (e.g.: Bool->Bool has size 2^2 = 4: not, id, const True, const False). > > So like you say, type negation corresponds to a continuation on that type > (where a continuation doesn't return any value at all, satisfying the empty > type). So ~A=A->_|_. That interpretation works out really well too, because > identities like A+B=~A->B can be read as compilation techniques for variants > (with the obvious construction and destruction approaches). > > But I'm not sure that I've got a straight story on this interpretation of > negation, quite. I think that it's suggesting that the size of the set of > continuations A->_|_ is |_|_|^|A|, or 0^|A|, which should be 0, right? So > there are 0 continuations -- they're impossible to construct? > > I appreciate any explanations y'all can offer on this point. > > Regards. > > > > On May 3, 2013, at 8:23 PM, Tadeusz Litak <[email protected]> wrote: > > > [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ] > > > > If I may chime in. The original point made by Uday re classical logic: > > > > >Coming to classical logic per se, I believe it is ill-fit for describing > > computer programs or "processes" > > > > is certainly worthy of attention. But it does not seem to imply the > > conclusion of that mail: > > > > >It is time to leave behind the classical logic. In fact, we should have > > done it a long time ago. > > > > (even if it wasn't intended, it does indeed sound "like a total and > > unconditional rejection"... such things happen in the fervor of a > > discussion :-) > > > > "Logical pluralism" is a position rather well-established in the philosophy > > of logic. I would think that in the context of Computer Science, it is even > > more tempting. > > > > [incidentally and perhaps contrary to established views, even Brouwer > > himself could be perhaps seen as one of first logical pluralists. While he > > very strongly rejected Fregean-Russellian logicism in *foundations of > > mathematics*, he has always held the work of Boole and the whole algebraic > > tradition in logic in high regard... But this is an aside] > > > > It might even happen to be Uday's own position, if I understand correctly > > the remark that "we can perfectly well circumscribe various regimens for > > various purposes." Most of my email will elaborate on this. > > > > > > I would simply say that whenever one wants, needs or has to think of all > > propositional formulas (also those possibly involving implication, and also > > those involving fusion, "tensor product" or what have you) as *rewritable > > to a conjunctive-disjunctive normal form without loss of information*, then > > the underlying domain logic is essentially classical. > > > > It is hard to imagine whole areas of Theoretical CS if rewriting formulas > > to CNF or proofs by contradiction/contraposition/excluded middle are > > suddenly deemed outdated and/or illegal... I mean not only and not even > > primarily logic programming, but also finite model theory, complexity > > theory, ontologies/description logics or the whole PODS/VLDB community... > > > > [actually, as a curious aside, the logic of database theorists, while > > certainly not constructive, is not fully classical either. They dread the > > top constant and unrestricted negation, preferring instead relative > > complement. This has to do with assumptions such as "closed world", "active > > domain" and the demand that queries are "domain independent". In short, > > their logic is rather that of Boolean rings without identity, > > which---funnily enough---also happen to be the setting of Stone's original > > work. It is just contemporary and ahistorical misrepresentation to say that > > Stone was working with "Boolean algebras". But this, again, is an aside...] > > > > And even in the context of Curry-Howard correspondence, classical logic is > > a legitimate setting to discuss languages with control operators, > > first-class continuations, static catch/throw a la Scheme etc. There is so > > much stunningly beautiful work in that community that deserves to be better > > known... > > > > > > But, equally obviously, not all the programming languages have such > > constructs. Furthermore, as linear logicians (already mentioned by Uday) > > will be happy to tell you, there are contexts when even intuitionistic > > notion of implication (so also the one of topos-theorists or > > proof-assistants, for example) is way too coarse-grained. Particularly when > > one wants, needs or has to be resource-aware. Also, the recent work of > > Wadler, Pfenning and other authors suggests that Curry-Howard > > correspondence for concurrency will have to do with linear rather than > > intuitionistic logic. > > > > > > [And as substructural logicians will be happy to tell you, there are > > contexts where even linear logicians may seem coarse-grained, > > thick-skinned, corner-cutting brutes. :-) But this, yet again, is an > > aside.] > > > > But where I most likely would part ways with Uday is when he claims (if I > > understand correctly) that we are approaching or even should approach "a > > final answer" of any kind. To me, searching for one logic valid in all > > CS-relevant contexts seems a rather misguided enterprise. Especially or at > > least when we talk about logic understood as a formal inference system. > > > > What we perhaps need is more introductory logic courses---and also > > handbooks and monographs---for budding CS undergraduates and graduates (and > > perhaps also some postgraduates) which would make them understand the > > subtlety and complexity of the picture. And the benefits and costs of > > adopting specific inference rules. > > > > Proof-assistant based courses seem to go in just the right direction. I am > > teaching right now one based on that excellent "Software Foundations" > > material of Benjamin Pierce et al. I think it changes and sharpens not only > > the thinking of students, but also that of the teacher himself (or herself > > :-). > > > > But even this only goes so far---after all, the underlying logic is > > essentially intuitionistic... on the other hand, any weaker one could > > quickly become a nightmare for actually discussing things as demanding as > > semantics of programming languages (with bangs and exclamation marks in > > every second lemma... :-) > > > > > > To conclude, a few minor points: > > > > > > > In fact, we cannot accept that we have a final answer until the entire > > > natural language has been formalized > > > > We'll wait for this only a little longer than for the invention of > > perpetuum mobile and heat death of the universe... :-) > > > > And which "natural language" are we talking about? Sometimes I think the > > only reason why, e.g., Chomsky ever came up with the idea of "universal > > grammar" was that he did not speak too many languages in the first place > > (although Hebrew seems reasonably distant from English)... > > > > > > > (The view I take, following Quine, is that logic is a regimentation of > > > natural language. > > > > Same objection as above, and this is just to begin with. > > > > [The only redeeming features of Quine were that he wrote well and had a > > certain logical culture. As a philosopher, in my opinion, he had a rather > > destructive influence on development of logic, particularly in philosophy > > departments, even if nowhere near as disastrous as the neopositivists or > > the majority of "analytic philosophers". But this is just one more aside...] > > > > > > > We can perfectly well circumscribe various regimens for various purposes. > > > > As said above, I'm perfectly in agreement with this statement. > > > > > > > > > I am entirely happy with the characterization of logical connectives as > > > "information composition" operators. But we can only accept it as a good, > > > but vague, intuition. We do not know what this "information" is. Neither > > > do we know what the information is about. So, in order to claim that > > > classical logic is a canonical information composition calculus, somebody > > > would need to formalize those notions. > > > > > > I think I can agree with every word here. Perhaps the difference then is > > not so big... > > > > I guess then that "leaving classical logic behind" meant rather "stop > > presenting it to students as the only, final and >>real<< formalism for > > Computer Scientists, everything else being a marginal pathology, if > > mentioned at all"... and if this was indeed intended by this remark, I > > would have a hard time disagreeing. > > > > Okay... back then to popcorn and a comfortable seat in the audience... > > > > Best, > > t. > > > > > >
