Talk:Lambda cube

This article is rated Start-class on Wikipedia's content assessment scale.
It is of interest to the following WikiProjects:

Mathematics Low‑priority

	Mathematics portal This article is within the scope of WikiProject Mathematics, a collaborative effort to improve the coverage of mathematics on Wikipedia. If you would like to participate, please visit the project page, where you can join the discussion and see a list of open tasks.MathematicsWikipedia:WikiProject MathematicsTemplate:WikiProject Mathematicsmathematics articles
Low	This article has been rated as Low-priority on the project's priority scale.

Computing

	This article is within the scope of WikiProject Computing, a collaborative effort to improve the coverage of computers, computing, and information technology on Wikipedia. If you would like to participate, please visit the project page, where you can join the discussion and see a list of open tasks.ComputingWikipedia:WikiProject ComputingTemplate:WikiProject ComputingComputing articles
???	This article has not yet received a rating on the project's importance scale.
	This article has been automatically rated by a bot or other tool because one or more other projects use this class. Please ensure the assessment is correct before removing the `\|auto=` parameter.

Untitled[edit]

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

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

LF isn't a system in the cube[edit]

\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)[reply]

Confusing[edit]

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)[reply]

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)[reply]

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)[reply]

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)[reply]

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)[reply]

lambda calculus is not strongly normalizing[edit]

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)[reply]

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

\cdot (interpunct)?[edit]

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)[reply]

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

Complete rewrite[edit]

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)[reply]

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)[reply]

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)[reply]

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

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)[reply]