Talk:Pure type system

Redirection Problem

I found a reference in another article (Curry's Paradox) to the page for Girard's Paradox, which kindled my curiosity: I wonder what that paradox is about. So I clicked the link, and I was redirected here (the article on Pure Type Systems). Instead of finding a detailed description of the paradox, I find an article on a different subject altogether, which includes a link to the Girard's Paradox page. Of course, clicking on it just takes you right back here all over again. What's going on? Was there ever a Girard's Paradox page? What happened to it? Hccrle (talk) 20:43, 31 August 2009 (UTC)

Girard's paradox is an analogue of the Kleene-Rosser paradox in some pure type systems (U and U^- to be precise). I think this stub makes that clear enough. In order to actually present the paradox, we need first the formal definition of a PTS, followed by the definitions of those two systems. Feel free to contribute (see todo list above). Pcap ping 05:00, 1 September 2009 (UTC)

LTU thread

Paper it points to might be useful: 67.119.3.55 (talk) 18:11, 3 June 2011 (UTC)

Apparent contradiction

The first paragraph says that there may be dependencies between any two pairs of sorts, but then gives an example in which this is stated to be not the case (the simply-typed lambda calculus).--greenrd (talk) 18:44, 12 May 2013 (UTC)

What's the contradiction? "May have dependencies" does not mean "must have depdendencies". Perhaps see lambda cube ? 99.153.64.179 (talk) 17:52, 25 June 2013 (UTC)

Intention unclear

"Pure type systems may obscure the distinction between types and terms and collapse the type hierarchy, as is the case with the calculus of constructions, but this is not generally the case, e.g. the simply typed lambda calculus allows only terms to depend on terms."

It's not clear where you're going with this. Everything up to this statement seems to imply that the simply typed lambda calculus is not a pure type system. Then, in the above quoted passage, you speak of pure type systems and the simply typed lambda calculus in the same breath. Since STLC is the weakest corner of the lambda cube, this statement seems rather trivial, not relevant, and in context quite possibly a bit misleading. If you were going somewhere with this, please find a way to reformulate it (possibly in its own section). If not, then removing the statement is probably the right course of action. Comiscuous (talk) 21:19, 28 December 2021 (UTC)

OpenAI has claimed to have partially proved the BGK conjecture mentioned in the article.

In september 2026, OpenAI released a lot of papers in their openai/math github repo, one of them ("Weak and strong normalization in pure type systems") covers the beta reduction case of the Barendregt-Guevers-Klop conjecture, and claims to have a correct lean formalization. I can't find secondary sources for this specific claim, so it looks like researchers in the field haven't peer reviewed it yet. Since this article lists it as one of the major open problems in math (with no other wiki articles mentioning the conjecture as far as I can tell), and other articles describing open problems that have claimed solutions in this group have made a mention of it, would it be worthwhile referring to it in the article? CcapitalK (talk) 14:06, 21 October 2026 (UTC)