You're reading the public-facing archive of the Category Theory Zulip server.
To join the server you need an invite. Anybody can get an invite by contacting Matteo Capucci at name dot surname at gmail dot com.
For all things related to this archive refer to the same person.
Suraaj K S (Aug 19 2024 at 00:51):I have been reading Mitchell's "Foundations for Programming Languages", and I am a little bit curious / confused about something..
The book does start off with 'logics' (first equational logic (aka Universal Algebra), and then the Simply Typed Lambda calculus). Moreover, once you have a logic, you can make a theory by having a signature and some axioms. For instance, using equational logic, and a single-sorted signature with a binary (composition) and unary (inverse) function symbols, we can specify the theory of groups.
In the book (example 4.4.7 to be precise), there is a 'way' of obtaining 'logic' as a theory from STLC (Simply Typed Lambda Calculus) by doing the following:
Then we have a bunch of axioms (which correspond to Church's theory of simple types).
In essence, we can present higher-order logic as a theory of λ-calculus (with just function types).
What surprises me is that I always equated STLC with 'boring' intuitionistic propositional calculus, which does not have 'forall's etc. I always thought we'd need a better logic (than STLC, with dependent types maybe?) to do 'forall's etc. But here, apparently, it seems like we 'can do' 'forall's in just STLC, by adding a whole bunch of 'meaningless' axioms. I'd be curious if this is a general/well-known technique? To me, it almost seems like we have 'set theory' be a theory of 'basic' equational logic by just forcing all theorems of set theory to be axioms.. Am I missing something?
I am just curious to hear any thoughts / remarks...
Ryan Wisnesky (Aug 19 2024 at 01:43):Higher order logic can indeed be defined as STLC + a type of propositions. The fact that you "only need one binder (lambda)" and other binders (such as forall) can be represented as constants is known as "lambda the ultimate" in programming language circles.
Kevin Carlson (Aug 19 2024 at 03:59):One way to see how this isn't quite as shocking as it initially seems is to think semantically. STLC has semantics in Cartesian closed categories, whereas lambda calculus plus the stuff you've added would have its most natural semantics in a topos. But you're not going to be able to assert that has any relationship to the set of monomorphisms into in terms of the STLC. Another way of thinking of this is that it's possible to give a notion of a topos internal to a finitely complete category, but that's quite different than the notion of a topos, and in general there will be models of the theory you've described here quite different than the intended examples where is an actual subobject classifier.
Suraaj K S (Aug 19 2024 at 23:42):I see. I'm curious whether I could take the idea further? Could I perhaps have "STLC" as a theory of equational logic?
Or could I think of it this way - in STLC, we could 'simulate' adding new rules of inference by just adding axioms of the form premise → conclusion?
Ryan Wisnesky (Aug 19 2024 at 23:52):Yes to the first question: the purely equational form of simply typed lambda calculus is sometimes called "categorical abstract machine language" and was the original intermediate form for the CAML compiler, which converted STLC with its variable-full syntax into variable-free terms in CAML and then optimized those terms using equations. CAML was superseded by other intermediate forms in compiling but is still a convenience language to use. The syntax of CAML is given here: https://en.wikipedia.org/wiki/Curry–Howard_correspondence#Curry–Howard–Lambek_correspondence .
Ryan Wisnesky (Aug 20 2024 at 00:01):Yes to the second question, but the catch is that there are a bunch of theorems about the STLC that only apply to closed terms; having axioms makes those theorems not apply. For example, "every closed term of type numeral reduces to a natural number" can be invalidated by an axiom stating "infinity exists". (this is a terrible example; this phenomenon also comes up in HoTT, where it is much more of a problem)
Suraaj K S (Aug 20 2024 at 00:32):Oh wow. This discussion really seems to blur the distinction between 'logics' and 'theories of a particular logic', and that makes me a little uncomfortable.. XD
Suraaj K S (Aug 20 2024 at 00:35):Kevin Carlson said:
STLC has semantics in Cartesian closed categories, whereas lambda calculus plus the stuff you've added would have its most natural semantics in a topos.
Here, is 'lambda calculus' different form STLC? In my question, I thought that they were the same...
Kevin Carlson (Aug 20 2024 at 02:49):I was not meaning to draw a distinction, no.
Kevin Carlson (Aug 20 2024 at 02:50):I might have spelled it out there because before some edit I was going to say something about dependently-typed lambda calculus, but then changed my mind.
Sam Staton (Aug 23 2024 at 08:57):Just to add, if I understand your question right @Suraaj K S, there are various successful mechanized proof systems that use this idea, such as HOL4 and Isabelle/HOL. For instance the HOL4 logic manual here.
Suraaj K S (Aug 24 2024 at 18:58):Sam Staton said:
Just to add, if I understand your question right Suraaj K S, there are various successful mechanized proof systems that use this idea, such as HOL4 and Isabelle/HOL. For instance the HOL4 logic manual here.
Thanks for your response. I was wondering if you could elaborate a little bit? Is the idea that you could have something like MLTT as a theory of HOL4?
Madeleine Birchfield (Aug 24 2024 at 19:09):Suraaj K S said:
Thanks for your response. I was wondering if you could elaborate a little bit? Is the idea that you could have something like MLTT as a theory of HOL4?
HOL4 and Isabelle/HOL are simple type theories, so don't really have anything to do with MLTT. Quote:
The reason for restricting to be closed, i.e. to have no free variables, is that otherwise for consistency the defined type operator would have to depend upon (i.e. be a function of) those variables. Such dependent types are not (yet!) a part of the HOL system
It is actually possible to have a dependent type theory like MLTT be a theory of higher order logic, by using the presentation of dependent type theory with a single type judgment and then adding a [[type of all propositions]] to the type theory along with the usual dependent product types, dependent sum types, identity types, and some form of infinity (such as the natural numbers).
But this is really only possible in the presentation of dependent type theory using a single type judgment. Most dependent type theories being used in the real world define types using an infinitely many Russell universes and zero type judgments or infinitely many Coquand universes and infinitely many type judgments, and then you no longer have a higher order logic because higher order logic doesn't really have an infinite number of universes.
Suraaj K S (Aug 27 2024 at 00:21):Kevin Carlson said:
But you're not going to be able to assert that σ→tv has any relationship to the set of monomorphisms into σ in terms of the STLC
I was wondering if this point could be elaborated? Why are we talking about monomorphisms here? (Sorry, I've just started learning this stuff, and I'm sure I might be asking something very trivial...)
Ryan Wisnesky (Aug 27 2024 at 00:32):One point of elaboration is that whereas STLC can be axiomatized equationally (the axioms are even written on wikipedia), the axiomatization of a topos is not purely equational, because the machinery required to define sub object classifiers includes concepts such as monos that are not purely equational (requiring implication). So STLC + a type prop + equations has a natural model in a topos, but is itself not a complete description of a "free" topos like how STLC + equations is a complete description of a "free" cartesian closed category.