Talk:Lambda cube

Untitled

This article would benefit from a diagram of the lambda-cube. --Malcohol 10:45, 25 May 2007 (UTC)

Beatriz Veronica 181.117.221.32 (talk) 06:33, 28 July 2023 (UTC)

LF isn't a system in the cube

\lambda P is, but LF isn't. LF and \lambda P, though closely related, are *not* the same. LF has a conversion rule that considers terms up to beta/eta equality, as opposed to only the beta equality in \lambda P. DPMulligan (talk) 19:29, 2 November 2010 (UTC)

Confusing

The article first lists three kinds of type systems (terms-types, types-types, types-terms), but then mentions twice the "eight calculi", and not three. --Gwern (contribs) 22:17 28 January 2008 (GMT)

What is meant is that there are three forms of abstraction potentially supported by type systems. Now, consider a unit cube: Clearly, each vertex has three coordinates. As such, type systems can be associated with a vertex of the cube according to which of the three forms of abstraction they support. That is, if they support a form, then the associated coordinate is a 1, otherwise 0. A diagram would help, I think... 65.183.135.231 (talk) 04:56, 9 November 2008 (UTC)

Oh, and of course a cube has eight vertices, so there are eight calculi. The one at (0,0,0) is really boring, though... 65.183.135.231 (talk) 04:57, 9 November 2008 (UTC)

If someone wants to make a cube graphic, there is an example of one at: http://www.rbjones.com/rbjpub/logic/cl/tlc001.htm. 65.183.135.231 (talk) 04:58, 9 November 2008 (UTC)

It's unfortunate that the cube is inconsistent with the text. I'm guessing that Lambda-2 is System F and Lambda-P is Lambda-Pi? (If I'm wrong, then it's even more confusing than I thought!). It might be good to somehow note the relationship.

It's not unfortunate, it's criminal. Can someone who knows tell us which of the pair of names for each system is generally accepted and/or canonical (with a citation) so someone can make the text match the cube. 98.118.43.182 (talk) 04:08, 2 December 2018 (UTC)

And it's even worse than that; the article switches names of systems _from section to section_. Could someone who knows _please_ fix this. 71.139.124.132 (talk) 01:11, 23 August 2020 (UTC)

lambda calculus is not strongly normalizing

The article currently states: all eight calculi are strongly normalizing, but this cannot be right, as one of the eight corners of the cube, the origin, is given as the untyped lambda calculus, which is not strong nor even weak normalizing. I don't know what the correction to this statement would be. linas (talk) 17:00, 5 July 2012 (UTC)

Never mind, misread "simply-typed" as "untyped", got confused. linas (talk) 16:40, 6 July 2012 (UTC)

\cdot (interpunct)?

Why does this article use \cdot for the separator between the parameter and the body of lambdas?

\cdot is variously associated with: multiplication, dot product, and placeholder (https://en.wikipedia.org/wiki/List_of_mathematical_symbols)

These articles: https://en.wikipedia.org/wiki/Calculus_of_constructions and https://en.wikipedia.org/wiki/Lambda_calculus both use simple period instead of \cdot. — Preceding unsigned comment added by 98.234.74.137 (talk) 19:15, 30 September 2019 (UTC)

Updated AhoChan (talk) 04:32, 1 October 2019 (UTC)

Complete rewrite

I tagged this article as needing a complete rewrite to hopefully draw attention from an expert who can fix the inconsistent names used in the text (sometimes between different sections of the text!) and the illustration of the eponymous lambda cube. Absent this correction, the article is _worse than useless_. 71.139.124.132 (talk) 14:22, 25 September 2020 (UTC)

I've been using the article as a supplement to other material (in particular some material referred to), and I don't see this article as needing a rewrite. The topic, in my opinion, is quite subtle and hard to grasp, but I can't immediately see major corrections or inconsistencies. In fact, there is even a correction in this article to a minor error made in the original paper by Barendregt. I certainly wouldn't call it _worse than useless_. Can you point out a few of the issues so I can see if I can correct or elaborate upon them? Nathan.s.chappell (talk) 13:10, 25 November 2022 (UTC)

At the time I wrote that, the diagram and the text (And the text, internally) had wildly varying names for the same systems; that much at least seems to have been corrected [though I've only quickly skimmed the diagram vs. the text] so 'complete rewrite' may no longer be (and may never have been) warranted. Thanks. 71.139.124.132 (talk) 21:57, 16 April 2023 (UTC)

Why is there a link to homotopy type theory in the 'See also' section?

I don't really see a justification for including a link to HoTT in this article. HoTT doesn't fit into the formalism of the Lambda cube; it isn't even a pure type system. The article doesn't mention Martin-Löf type theory or identity types.

The link feels like an inclusion motivated by a desire to promote HoTT, rather than something with a legitimate informative purpose. Hames Janson (talk) 20:38, 24 January 2024 (UTC)

Is 'a' a variable or a term in the Application rule?

The second assumption in the Application inference rule says $\Gamma \vdash a:A$. Lowercase letters everywhere else are variables, but I think here it should be a term. If we change $a$ to $D$, is the rule still correct? Metaweta (talk) 18:46, 6 September 2024 (UTC)

Yes, according to https://cs.stackexchange.com/a/169636/174020 Metaweta (talk) 22:47, 7 September 2024 (UTC)

Why is the assumption Γ ⊢ B':s necessary in the Conversion rule?

Is it possible to derive a judgement $\Gamma \vdash A:B$ when $B$ is not a sort? If not, is it possible for $B$ to be a sort and have $B=_{\beta }B'$ but have $B'$ not be a sort? Metaweta (talk) 18:51, 6 September 2024 (UTC)

Asked on StackExchange and got an answer: the assumption is not strictly necessary (it could be proven as a theorem) but it's useful. Metaweta (talk) 19:41, 7 September 2024 (UTC)

Is reduction under λ necessary?

Most programming languages don't do reduction under a lambda. What happens if we remove the rule ${\frac {B\to _{\beta }B'}{\lambda x:A.B\to _{\beta }\lambda x:A.B'}}$? Metaweta (talk) 18:57, 6 September 2024 (UTC)

It's part of a process for learning how to understand a statement, using abstract rewriting. See for example Amar Shah (2017) e.g. learn eta reduction, learn combinators -- Ancheta Wis   (talk | contribs) 08:31, 7 September 2024 (UTC)

I know what the inference rule means. I'm asking if removing the rule causes any problems rather than merely a weaker type system. As far as I can tell, the only place beta equivalence is used in the inference rules is in Conversion. There will be terms $A\colon B$ where $B$ used to be beta-equivalent to $B'$ so we could derive that $A\colon B'$ under the old rules, and now can't prove that; but I don't think it introduces any inconsistency. Metaweta (talk) 19:49, 7 September 2024 (UTC)

In the Start rule, why can't x appear in Γ?

It looks to me like we can introduce x twice by beginning with Start and then using Weakening. Why then have the side condition on Start? Metaweta (talk) 19:15, 16 October 2024 (UTC)

In both of these lecture notes (1, 2), there's the same side condition on the Weakening rule. Without that side condition, this stack exchange answer shows that the system is unsound. Metaweta (talk) 19:07, 17 October 2024 (UTC)

Images related to "Lambda cube" are missing.

Please review the images on the web page of the following network link and add the necessary ones to the "Lambda cube" article:

https://www.google.com/search?q=lambda+cube&udm=2 78.190.206.8 (talk) 08:49, 29 October 2024 (UTC)

Added request template to this page.--Commander Keane (talk) 11:40, 29 October 2024 (UTC)