A Lambda Cube is a conceptual framework in the field of computer science and logic that represents the relationships between different typed lambda calculi. It was first introduced by [[Henk Barendregt]] in 1992 as a way to categorize and study various forms of lambda calculi.  The Lambda Cube consists of three dimensions, each representing a different aspect or extension of the lambda calculus: 1. Simply Typed Lambda Calculus (λ→): This is the simplest form of lambda calculus, where functions are defined on typed variables. It has a single type, known as the arrow type (→), which represents function types. The simply typed lambda calculus provides the foundation for more complex lambda calculi. See [Lambda Cube on Software Foundations of Benjamin Pierce](https://softwarefoundations.cis.upenn.edu/plf-current/Stlc.html) 2. Polymorphic Lambda Calculus (λ2): This dimension extends the simply typed lambda calculus by introducing polymorphism. In this system, types can be parameterized over other types, allowing for more general and reusable code. 3. Higher-Order Lambda Calculus (λω): This dimension extends the polymorphic lambda calculus by introducing higher-order functions and types. Higher-order functions can take other functions as arguments or return them as results, while higher-order types can be parameterized over functions. The combination of these three dimensions results in eight points in the Lambda Cube, each representing a different combination of features: - λ→: The simply typed lambda calculus with no additional features. - λ2: The polymorphic lambda calculus without higher-order functions. - λω: The higher-order lambda calculus without polymorphism. - λP: The simply typed lambda calculus with both polymorphism and higher-order functions. - λ2ω: The polymorphic higher-order lambda calculus. - λPω: A system that combines all three features but restricts polymorphism to only first-order types. - λΩ: A system that combines all three features without any restrictions on polymorphism. - Ω: A system that allows for unrestricted higher-order functions but does not have explicit typing. # Relation to System F The Lambda cube is a framework for understanding and categorizing different type systems in lambda calculus. It was introduced by Henk Barendregt in the 1980s. [[System F]], also known as the polymorphic lambda calculus, is one of the most well-known type systems within the Lambda cube. It extends the simply typed lambda calculus with universal quantification, allowing the definition of polymorphic types and functions. In terms of the Lambda cube, System F corresponds to the second dimension, known as System F or Girard's System F. This dimension is characterized by introducing polymorphism through universal quantification. The types in this dimension can be seen as having more expressive power than those in the previous dimension, known as simply typed lambda calculus. Overall, System F is a specific instantiation of one of the dimensions in the Lambda cube framework. # Lambda Cube and Rubiks Cube According to Bing's chat: > I’m not aware of any direct relationship between Lambda cube and Rubik’s cube. Lambda cube is a formal system used to study the foundations of programming languages, while Rubik’s cube is a mechanical puzzle that challenges one’s spatial reasoning and problem-solving skills. However, there are some interesting connections between the two concepts that can be explored. > For instance, one could use the Lambda cube to model the Rubik’s cube as a functional program. The cube could be represented as a data structure, and the operations required to solve it could be expressed as functions that manipulate this structure. This would allow us to reason about the properties of the Rubik’s cube in a more abstract and mathematical way. > Another possible connection is through the use of algorithms. Both Lambda calculus and Rubik’s cube algorithms are based on the idea of applying a sequence of operations to achieve a desired result. In the case of Lambda calculus, these operations are reductions that simplify expressions, while in the case of Rubik’s cube algorithms, they are rotations that move pieces into their correct positions. > While there may not be a direct relationship between Lambda cube and Rubik’s cube, exploring these connections can help us gain a deeper understanding of both concepts. # Conclusion The Lambda Cube provides a framework for understanding the relationships and expressive power of different lambda calculi. It has been used to study the type systems of programming languages, formalize logical systems, and explore the foundations of computation. ## SUMMARY by Fabric A group of students from the Technical University of Berlin, under Professor [[Uwe Nestmann]], introduces the lambda calculus and type theory through a video series titled "The Lambda Cube Unboxed." ## IDEAS: - Lambda calculus serves as a foundational model for computation and functional programming. - Type theory offers a rich framework for understanding computation and logic. - The lambda cube organizes type systems in a three-dimensional conceptual space. - Untyped lambda calculus is presented as equivalent to Turing definable functions. - Simply typed lambda calculus adds basic types to enhance the untyped version. - Extensions of simply typed lambda calculus lead to three distinct type systems. - The Curry-Howard isomorphism links type theory with mathematical logic intriguingly. - Real-world programming languages incorporate concepts from lambda calculus and type theory. - The series aims to provide an overview and encourage further personal research. - Exercises in type theory and formal proof deepen understanding through practice. - Exploring programming languages helps apply theoretical concepts in practical contexts. - Revisiting the video series can reveal new insights and connections. - The lambda cube's structure illustrates the evolution of type systems. - Functional programming and proof assistants are grounded in lambda calculus. - Theoretical aspects of polymorphic lambda calculi are explored in recommended papers. - The complexity of the topic grows with deeper exploration into sub-areas. - The video series is inspired by foundational texts and talks in the field. - Viewers are encouraged to engage with the material actively through exercises and experimentation. - The series provides a starting point for exploring complex topics in computation. - Understanding the lambda cube requires grasping both mathematical and programming perspectives. - The series is designed to spark curiosity and guide viewers toward further study. ## INSIGHTS: - Lambda calculus bridges the gap between abstract computation models and practical programming languages. - Type theory's evolution is visualized through the conceptual framework of the lambda cube. - Engaging with theoretical concepts through exercises enhances comprehension and application skills. - Re-exploration of educational content can deepen understanding and uncover new insights. - Theoretical computer science connects deeply with real-world applications through type systems. - The Curry-Howard isomorphism exemplifies the profound connections between logic and computation. - Active learning approaches, such as exercises and programming, solidify theoretical knowledge. - The complexity of lambda calculus and type theory reflects their broad applicability and depth. ## QUOTES: - "Lambda calculus serves as a foundational model for computation and functional programming." - "Type theory offers a rich framework for understanding computation and logic." - "The lambda cube organizes type systems in a three-dimensional conceptual space." - "Untyped lambda calculus is presented as equivalent to Turing definable functions." - "Simply typed lambda calculus adds basic types to enhance the untyped version." - "Extensions of simply typed lambda calculus lead to three distinct type systems." - "The Curry-Howard isomorphism links type theory with mathematical logic intriguingly." - "Real-world programming languages incorporate concepts from lambda calculus and type theory." - "The series aims to provide an overview and encourage further personal research." - "Exercises in type theory and formal proof deepen understanding through practice." - "Exploring programming languages helps apply theoretical concepts in practical contexts." - "Revisiting the video series can reveal new insights and connections." - "The lambda cube's structure illustrates the evolution of type systems." - "Functional programming and proof assistants are grounded in lambda calculus." - "Theoretical aspects of polymorphic lambda calculi are explored in recommended papers." - "The complexity of the topic grows with deeper exploration into sub-areas." ## HABITS: - Engaging with exercises in type theory to deepen understanding of abstract concepts. - Actively applying theoretical concepts in programming languages to see their practical use. - Re-watching educational content to uncover insights missed during the first viewing. - Encouraging self-directed research to explore topics of personal interest further. - Practicing active learning by working on exercises related to lambda calculus. - Exploring both mathematical and programming perspectives to gain a comprehensive understanding. - Seeking out additional resources like papers and books to expand knowledge base. - Engaging in discussions with peers to share insights and learn collaboratively. ## FACTS: - Lambda calculus is a foundational model for computation equivalent to Turing machines. - Type theory encompasses both computation models and mathematical logic frameworks. - The lambda cube provides a structural visualization of different type systems' evolution. - Real-world programming languages are influenced by concepts from lambda calculus and type theory. - The Curry-Howard isomorphism demonstrates a deep connection between logic and computation. - Functional programming languages are directly grounded in lambda calculus principles. - Theoretical computer science explores complex topics like polymorphic lambda calculi. ## REFERENCES: - "Type Theory and Formal Proof: An Introduction" by Rob Nienhuis and Hermann Geuvers - "[[@LambdaCalculusTypes2013|Lambda Calculus with Types]]" by [[Henk Barendregt|H.B. Barendregt]] - "[[@wadlerPropositionsTypes2015|Propositions as Types]]" by [[Philip Wadler]] - "Proofs and Types" by Jean-Yves Girard, translated by Paul Taylor and Yves Lafont - "Programming in Higher Order Typed Lambda Calculi" by Benjamin Pierce, Scott Dietzen, Spyro Mikhailov ## ONE-SENTENCE TAKEAWAY: Explore the foundational models of computation through lambda calculus to enhance both theoretical understanding and practical programming skills. ## RECOMMENDATIONS: - Engage with exercises in type theory for deeper understanding of abstract concepts. - Apply theoretical concepts in programming languages to see their practical use. - Re-watch educational content to uncover insights missed during the first viewing. - Conduct self-directed research to explore topics of personal interest further. - Work on exercises related to lambda calculus for active learning benefits. # References ```dataview Table title as Title, authors as Authors where contains(subject, "Lambda Cube") or contains(subject, "lambda cube") or contains(title, "Lambda Cube") or contains(title, "lambda cube") ```