Blurring the distinction between functional programming and proof theory is wonderful but, in your case, it seems to have generated more confusion than anything. You may have heard about the Curry-Howard correspondence and the fact that the $\lambda$-calculus and type theory are deeply connected, which is great, but is not necessarily the preferred route from your point of view. Second: you seem to be interested in the $\lambda$-calculus as a programming langage, which means you can safely ignore (at least on a first approach) its connections to intuitionistic logic. The fact that your theory is intuitionistic doesn't mean that your meta-theory has to be! You may freely use proof by contradiction or the axiom of choice in order to prove results about the $\lambda$-calculus (people do that all the time). You seem to be confusing several things here.įirst of all, like Alexis said in her answer, I don't see why you would need to accept/reject the principles of a given logical theory in order to study it and learn about it.
If they even answer my question, would you mind explaining to me how (as if I were five, so to speak)? I don't quite understand the discussions on them.
Heyting algebra in simply typed lambda calculusĬan boolean algebra be expressed in simply typed lambda caclulus? These questions might be relevant: Where is the proof that Coq + Excluded Middle is consistent Also I thought Boolean functions were a very hot topic of computer science research, so it seems kind of strange that some computer scientists would prefer Heyting algebra. Ideally I would prefer to not have to choose between $\lambda$-calculus and Boolean algebra, since the latter underlies most of my understanding of logic, and is also the basis for probability theory, which I know very well and would not like to give up or reject as half-baked.
I read somewhere else (I forgot where unfortunately), that Heyting algebra is what results if one rejects the Law of the Excluded Middle, and thus presumably founding logic upon Boolean algebra means accepting the Law of the Excluded Middle. The discussion on p.9 of the Homotopy Type Theory book seems to say something to the effect that Univalent Foundations and Homotopy Type Theory can be compatible with the Law of the Excluded Middle and the Axiom of Choice, even though they contradict the univalent axiom? Needless to say I did not quite understand the argument about (-1) types and thus am still somewhat skeptical and unconvinced.Īlso, in one of his lectures at the Oregon Programming Language Summer School posted on youtube, Professor Awodey, one of the big names behind the IAS's Homotopy Type Theory/Univalent Foundations Project, seems to identify the Heyting algebra as underlying logic, rather than the Boolean algebra. Is there a way to learn about $\lambda-$calculus and type theory while at least being agnostic about the Law of the Excluded Middle and not outright rejecting it?
Perhaps that makes me old-fashioned, and my grandkids will laugh at me for this concern, but proof by contradiction can be very useful and is how I learned a lot of the math which I know. My background is more in mathematics than computer science, so although I can see how having to construct something to prove that exists is an acceptable restriction for people interested primarily in computation, I am really uncomfortable with having to give up proof by contradiction and the Law of the Excluded Middle. However, I just learned that type theory, at least as stated by Lof, is supposed to be a way to formalize intuitionistic logic/constructive mathematics, which rejects the Law of the Excluded Middle and even the Axiom of Choice. Also other reasons, like wanting to learn and understand functional programming, in order to have an alternative to C++ which I dislike. I want to learn about lambda calculus because it seems like an interesting way to think about functions in general, and because a generalization called the stochastic $\pi$ calculus studied by Luca Cardelli and others seems to allow many computational interpretations of biology, something which I am really interested in. I know very little about what I am talking about in what follows, so I appreciate any all help in pointing out all of my mistakes - otherwise I won't be able to learn more and advance in my knowledge of these interesting subjects.
0 kommentar(er)
