https://risingentropy.com/how-to-draw-lambda-diagrams/ Skip to content Rising Entropy Learn with me! Menu * Home * Archives * Post Guide * About * Contact How to draw lambda diagrams July 6, 2020 ~ squarishbracket If you don't want spoilers for my puzzle a few days ago, don't read ahead! I think lambda diagrams are extremely cool, and haven't seen any detailed description on how they work online. I'll start by showing some very simple examples of lambda diagrams, and then build up to more complicated ones. First of all, what are lambda diagrams? They are pictorial representations of lambda expressions, and hence count as a pictorial system for a large portion of mathematics. I will assume that you understand how lambda calculus works for this post, and if you aren't familiar then you can do no better than this video for a basic introduction. The Basics Let's start simple: the lambda expression for "True": lx.ly.x Each time we see a new bound variable, we draw a horizontal line to represent that variable. So parsing from left to right, we start with a horizontal line for x. [Lambda-Pics-2-1-] Next is "ly.", so we insert another horizontal line for y (below the first horizontal line). [Lambda-Pics-3-50] Next we have an x in the function body, which we represent by a vertical line leaving the x line: [Lambda-Pics-4-1] And there we have it, the lambda diagram for True! Now let's look at False: lx.ly.y We start the same way as before, with two horizontal lines for our variables x and y: [Lambda-Pics-3-50] But now we have a y in our function body, not an x. So we draw our vertical line leaving the y line instead of the x line: [Lambda-Pics-5-] And that's the diagram for False! The actual diagram needn't have the labels "x" and "y" in it, because our convention that we draw lines for new variables below existing horizontal lines uniquely specifies which lines stand for which variables. Let's now do a slightly more complicated function: lx.ly.y x As before, we start with our two variables, x and y. [Lambda-Pics-3-50] Now we have a y in the function body, so we add a vertical line leaving the y bar: [Lambda-Pics-5-] Next is an x, which is being fed as input to the y. We draw this as follows: [Lambda-Pics-7-4] Two things have happened here: First I've moved the original vertical line for y over to the left to make space. Next, I've represented "feeding x to y as input" as a line leaving the x bar and terminating at the vertical line for y. Take a guess what lx.ly.x y would look like! ... ... ... Here it is: [Lambda-Pics-8-1-] Next, let's look at lx.ly.x x y (which is incidentally the "or" function). We start with the introduction of the variables x and y. [Lambda-Pics-3-50] Next, an x: [Lambda-Pics-4-1] And another x: [Lambda-Pics-10-1] And finally a y: [Lambda-Pics-11-71] Notice that this y connects below the first connection, to the original branch. What would it mean if it were connected to the second branch? [Lambda-Pics-12-30131] As you can see, this would indicate that y is first fed to x, and then the result of THAT is fed to x. With these principles, you should now be able to draw out diagrams for much more complicated lambda expressions. Try this one: lx.ly.lz.z (y x) (y z x) x ... ... ... Here it is! [Lambda-Pics-13-3298696808-1594059] Make sure that this makes sense before moving on! Lambda Expressions within Lambda Expressions Next, we'll look at how to deal with lambda expressions that contain new lambda expressions within their function body. Here's a simple example: lx.ly.x (lz.z) y Everything up until the third l is the same as always: [Lambda-Pics-4-1] Now, to deal with our new variable z, we draw a new horizontal line. But importantly, this horizontal line comes after the vertical line for the x that has already been used! [Lambda-Pics-15-771603293-15] After the "lz." we have a "z", so we draw a line from the z bar to our original vertical line leaving x. [Lambda-Pics-14-1526369227] And finally, after all of this we feed y to the original vertical line: [Lambda-Pics-16-3035949799-] Try this one: lx.ly.x (lz.z z) (lw.lv.v (w w)) y [Lambda-Pics-19-608958326-1594062055570] And here's another one, where the inside function uses outside variables: lx.ly.x (lz.y z) [Lambda-Pics-17-328753828] Alright, the final category you need to know to understand how to draw any lambda diagram whatsoever is... Function Application Suppose we have the lambda expression (lx.ly.x) (lz.z z). We first draw the lambda diagrams for each of the two component expressions side by side: [Lambda-Pics-20-1991908369-159406252] And now we simply attach the second to the first, indicating that the entire second lambda expression is fed as input to the first! [Lambda-Pics-21-29174919-15940626] Here's another example for you to try: (lx.x) (ly.lz.z z y) (lw.lv.v (v w)) [Lambda-Pics-22-2561965373-1594063893937] And one more example, this one using all the tricks we've seen so far: (lx.x (ly.lz.z y y) (lw.lv.w (v x))) (lu.u u) [Lambda-Pics-23-4021505451-1594064762394] Beta Reduction The final thing to know about lambda diagrams is how to actually do computations with them. The basic idea is that when we have one lambda diagram fed as input to another, we can substitute the "input" diagram for each vertical line leaving the topmost horizontal bar, and then erase this bar. Let's look at some examples: [107018153_302325840822989_294562356102349335_n-2894004994-1594065242579] [106812956_1535071696651352_5977005141032762778_n-2485795303-1594065223703] You can also do function application within larger lambda diagrams. Take a look at the following example, which is a calculation that shows that the successor of zero is one: [106636569_3228505000533624_7353489861790611437_n] The first beta reduction here is just like the previous ones we've seen. But the second one does a substitution within the main lambda expression, as does the third. This works in much the same way as the earlier reductions we saw, the primary difference being that references to variables outside the scope of the function being applied must be maintained. You can see this in the final step above, where we remove the line representing the variable y, and attach the line connecting to it to the line representing the variable x. Now for the fun part! I've found some great animations of calculations using lambda diagrams on Youtube. Each of them is using just the rules I've described above, nothing more! And I must say that the music is delightful. Take a look! Beautiful! Share this: * Click to share on X (Opens in new window) X * Click to share on Facebook (Opens in new window) Facebook * Like this: Like Loading... Posted in Logic, Mathematics, Puzzle lambda calculuslogic Post navigation < PreviousFundamentals of Logic: Syntax, Semantics, and Proof Next >Pictures of some extremely large numbers 7 thoughts on "How to draw lambda diagrams" 1. Pingback: Undecidability results on lambda diagrams - Rising Entropy 2. [] Anonymous says: March 23, 2025 at 8:18 pm I feel enlighten Loading... Reply 3. [] Anonymous says: March 23, 2025 at 11:06 pm It looks like in the diagram right before beta reduction we call on w twice, but the formula only call once, right? Loading... Reply 4. [] Anonymous says: March 27, 2025 at 2:54 pm Am I mistaken or is the drawing of the diagram for (lx.x (ly.lz.z y y) (lw.lv.w (v x))) (lu.u u) instead one for (lx.x (ly.lz.z y y) (lw.lv.(w w) (v x))) (lu.u u)? Loading... Reply 1. [3e5d3d3] squarishbracket says: April 13, 2025 at 12:14 pm No you are correct, that was my mistake. Thanks for the correction! Loading... Reply 5. [34ba7e8] da lan says: March 30, 2025 at 6:40 pm amazing! Loading... Reply 6. [] Anonymous says: April 17, 2025 at 9:09 am Clean, great intro ! I'd love to see more ! Loading... Reply Leave a ReplyCancel reply Search for: [ ] [Search] Recent Posts * How hard is classification? Equivalence relations and Borel reductions * Choosing things is hard: infinite hats, definability, and topology * The Hypergame Paradox * ZFC as One of Humankind's Great Inventions * Hilbert-type Infinitary Logics * Forcing and the Independence of CH (Part 2) * Forcing and the Independence of CH (Part 1) * The Ultra Series: Guide * Shorter Proof of Countable Saturation (Ultra 7.5) * All About Countable Saturation (Ultra Series 7) * Ultraproducts and Compactness (Ultra Series 6) * Infinitely Large Primes (Ultra Series 5) * Ultraproducts and Los's Theorem (Ultra Series 4) * Hypernaturals in all their glory (Ultra Series 3) * Hypernaturals Simplified (Ultra Series 2) * Ultrafilters, Ultraproducts, and Hypernaturals 1: Introduction * Even Numbers are Tautologies * Notes on motivation and self-improvement * First Order Truth Trees * One nonstandard is worth infinitely many standards * This post is lying to you * Some half-baked thoughts on moral arbitrariness * Asymmetry between the infinite and finite * PA doesn't trust its provability predicate * No more than half of anti-sets are big * A Dating Puzzle, and Bayesian Experimental Design * What precedent does the Trump Twitter ban set? * Divisibility Tricks and Orderly Numbers * What's the probability that an election winner leads throughout the entire vote? * Quantum Chess * Biblical inerrancy * Formal Semantics 1: Historical Prelude and Compositionality * Two more short and sweet proofs of propositional compactness * The Theory of Knots * A Compact Proof of the Compactness Theorem * ZFC, and getting the right answer by accident * Polish Notation and Garden-Path Sentences * Defining uncountability * Who would win in a fight, logic or computation? * Computing truth values of sentences of arithmetic, or: Math is hard * How uncomputable are the Busy Beaver numbers? * The Arithmetic Hierarchy and Computability * A Self-Interpreting Book * Epsilon-induction and the cumulative hierarchy * Nonstandard integers, rationals, and reals * Transfinite Nim: uncomputable games and games whose winner depends on the Continuum Hypothesis * A Coloring Problem Equivalent to the Continuum Hypothesis * No known unknowns in Peano arithmetic * The subtlety of Godel's second incompleteness theorem * Undecidability results on lambda diagrams * The Anti-Set Program * Pictures of some extremely large numbers * How to draw lambda diagrams * Fundamentals of Logic: Syntax, Semantics, and Proof * The Pictorial Mathematics of Klak-Adbmal * The Rise of Anti-Set Theory * The Transfinite Factorial * On Self-Hating Theories of Arithmetic * Updated Introduction to Mathematical Logic * Finiteness can't be captured in a sound, complete, finitary proof system * The Mindblowing Goodstein Sequences * Wacky Non-Standard Models of PA * The Continuum Hypothesis is False * Kolmogorov Complexity, Undecidability, and Incompleteness * Constructing the Church-Kleene Ordinal * What ordinals can be embedded in Q and R? * Visualizing the rationals * The order type of the rational numbers * Can you compute all the countable ordinals? * Immoral or Inconsistent? * Constructing ordinal numbers in ZFC * Meaning ain't in the brain * On philosophical progress * Logic on Planet Zorko * A result on the incompleteness of mathematics * A Godelian Logic Puzzle * Crazy conditionals * A Dice Puzzle * Proving the Completeness of Propositional Logic * Sum and Product Puzzle * Four Pre-Godelian Limitations on Mathematics * A proof of the Compactness Theorem * A challenge to constructivists * Describing the world * The full solution to the dog puzzle * The Surprise-Response Heuristic * Three paradoxes of self-reference * A logic puzzle about dogs * A suspicious proof of God's existence * Fractal Trees * In defense of collateralized debt obligations (CDOs) * Six Case Studies in Consequentialist Reasoning * Will we ever build a Galactic Empire? * Earning to give or waiting to give * Diversification is magic * Paradoxical Precommitment * Solving the Linear Cournot Model * Building an analog calculator * Complex numbers in physics * The laugh-hospital of constructive mathematics * Can chess be solved? * For Loops and Bounded Quantifiers in Lambda Calculus * There's a problem with infinity * A Supertask Puzzle * Can an irrational number raised to an irrational power be rational? * Are the Busy Beaver numbers independent of mathematics? * Introduction to Mathematical Logic (Part 4: Zermelo-Fraenkel Set Theory) * The Weirdest Consequence of the Axiom of Choice * Introduction to Mathematical Logic (Part 3: Reconciling Godel's Completeness And Incompleteness Theorems) * Introduction to Mathematical Logic (Part 2: The Natural Numbers) * Introduction to Mathematical Logic (Part 1) * Thinking in first order: Are the natural numbers countable? * The Central Paradox of Statistical Mechanics: The Problem of The Past * Is The Fundamental Postulate of Statistical Mechanics A Priori? * The Necessity of Statistical Mechanics for Getting Macro From Micro * A Cognitive Instability Puzzle, Part 2 * Logic, Theism, and Boltzmann Brains: On Cognitively Unstable Beliefs * Philosophers of religion are religious. Why? * Why do prediction markets work? * A Talmudic Probability Puzzle * Galois' Unsolvable Polynomials * x^5 - x - 1 * Group Theory: The Mathematics of Symmetry? * Symmetries of Platonic Solids * Some Curious Group Isomorphisms * Extending Cauchy's Theorem * Strong Induction Proofs of Cauchy's Theorem and Sylow's First Theorem * Table of Small Finite Groups * Some Group Factoids * Group Theory Toolkit * The sweet spot on the structure spectrum * Proving Cauchy's Theorem * Group Theory: Lagrange's Theorem and the Sudoku Principle * The Most Irrational of Numbers * All About Adultery, BDSM, and Divorce * Collatz Tree * Record-breaking Collatz chains! * Producing all numbers using just four fours * A sequence prediction puzzle * Buddhabrot, Mandelbrot's older sibling * Hopping Midpoints * Exploring Julia Sets * Mandelbrot Exploration * How will quantum computing impact the world? * Hopping Midpoints and Mathematical Snowflakes * Backwards induction and rationality * Firing Squads and The Fine Tuning Argument * The EPR Paradox * Measurement without interaction in quantum mechanics * Is the double slit experiment evidence that consciousness causes collapse? * Decoherence is not wave function collapse * On decoherence * The problem with the many worlds interpretation of quantum mechanics * Consistently reflecting on decision theory * Decision Theory * Rationality in the face of improbability * A probability puzzle * Solving the common knowledge puzzle * A common knowledge puzzle * The history of lighting technology * Kant's attempt to save metaphysics and causality from Hume * Deriving the Lorentz transformation * Swapping the past and future * Visualizing Special Relativity * Fractals and Epicycles * How to Learn From Data, Part 2: Evaluating Models * How to Learn From Data, Part I: Evaluating Simple Hypotheses * The Match Problem * Godel's Second Incompleteness Theorem: Explained in Words of Only One Syllable * Anti-inductive priors * Making sense of improbability * A simple probability puzzle * The end goal of epistemology * Deciphering conditional probabilities * The Problem of Logical Omniscience * Sapiens: How Shared Myths Change the World * Anthropic reasoning in everyday life * Adam and Eve's Anthropic Superpowers * Sleeping Beauty Problem * Infinities in the anthropic dice killer thought experiment * Not a solution to the anthropic dice killer puzzle * Pushing anti-anthropic intuitions * An expected value puzzle * Dialogue from Kafka On The Shore * A closer look at anthropic tests for consciousness * Two principles of Bayesian reasoning * Explaining anthropic reasoning * Predicting changes in belief * In favor of anthropic reasoning * Clarifying self-defeating beliefs * Getting empirical evidence for different theories of consciousness * Bad Science Reporting * The Anthropic Dice Killer * What do I find conceptually puzzling? * More on quantum entanglement and irreducibility * Ramanujan's infinite radicals * Communication through entanglement * Quantum mechanics, reductionism, and irreducibility * Building the diffusion operator * Building the quantum oracle * Grover's algorithm * Deutch-Josza Algorithm * More on quantum gates * Quantum Computing in a Nutshell * Matter and interactions in quantum mechanics * 100 prisoners problem * Some simple probability puzzles * Deriving the Schrodinger equation * On existence * Concepts we keep and concepts we toss out * Seeing, Doing, Imagining * Against moral realism * Explanation is asymmetric * Wave function entropy * Query sensitivity of evidential updates * Summarizing conscious experience * Simple induction * The North Korea problem isn't solved * Priors in the supernatural * Patterns of inductive inference * If all truths are knowable, then all truths are known * Variational Bayesian inference * The value of the personal * Confirmation bias, or different priors? * Objective Bayesianism and choices of concepts * A shameful history * "Beating the drum for justice" * Overemphasizing disagreement * Regularization as approximately Bayesian inference * Against the status quo * Why minimizing sum of squares is equivalent to frequentist inference * History is Lamarckian * Short and sweet proof of the f(xy) = f(x) + f(y) logarithmic property * Constructing the world * Moving Naturalism Forward: Eliminating the macroscopic * Some social justice factoids * What is integrated information? * How to sort a list of numbers * Defining racism * Utter confusion about consciousness * Getting evidence for a theory of consciousness * The Scourge of Our Time * The problem with philosophy * Argument screens off identity * Facts about guns * "You don't believe in the God you want to, and I won't believe in the God I want to" * Galileo and the Schelling point improbability principle * Why "number of parameters" isn't good enough * Bayesian Occam's Razor * All about IQ * A model selection puzzle: Why is BIC [?] AIC? * Bayes and overfitting * The basics of information divergence * More model selection visualizations * Where I am with utilitarianism * The Monty Hall non-paradox * Akaike, epicycles, and falsifiability * On complexity and information geometry * A note of ambiguity regarding model selection * Gibbs' inequality * Some simple visual comparisons of model selection techniques * Bayes and beyond * Racism and identity * What is bias? * Value beyond ethics * Taxonomy of infinity catastrophes for expected utility theory * Two-factor markets for sex * A simple explanation of Bell's inequality * Cults, tribes, states, and markets * Bayesian experimental design * Why relative entropy * A survey of entropy and entropy variants * Entropy is expected surprise * The Rival-Expert Heuristic * Inference as a balance of accommodation, prediction, and simplicity * Pascal's mugging * Those who have forgotten words * Why systematize epistemology? * Journey into abstraction * Timeless decision theory and homogeneity * Timeless ethics and Kant * A failure of Bayesian reasoning * Bayesianism as natural selection of ideas * Against falsifiability * Metaphysics and fuzziness: Why tables don't exist and nobody's tall * Is [insert here] a religion? * Hyperreal decision theory * Infinite ethics * More on random sampling from Nature's Urn * Free will and decision theory (Part 2) * Paradoxes of infinite decision theory * Does fine-tuning give evidence for God? * Noisy Evidence * Nature's Urn and Ignoring the Super Persuader * Entropy vs relative entropy * Fun with Akaike * Anthropic argument for common priors * Why you should be a Bayesian * Consistency and priors * Dutch book arguments * Cox's theorem * Maximum Entropy and Bayes * Advanced two-envelopes paradox * Sam Harris and the is-ought distinction * Two envelopes paradox * Principle of Maximum Entropy * Consciousness * Inequality and free markets * 40 papers on inequality in one sentence each * Gregory Watson (and how to change the world) * Statistical mechanics is wonderful * Solution: How change arises in QM * TIMN view of social evolution * Race, Ethnicity, and Labels * Is quantum mechanics simpler than classical physics? * Iterated Simpson's Paradox * Causal decision theory * Free will and decision theory * Simpson's paradox * Screening off and explaining away * Societal Failure Modes * Dialogue: Why you should one-box in Newcomb's problem * Opt-out organ donation * The spiritual and the scientific * Comprehensibility of the Complex * Correlation and causation * Causal Intervention * Causal Arrows * Causality: Preliminaries * Low-hanging policy fruit Discover more from Rising Entropy Subscribe now to keep reading and get access to the full archive. Type your email... [ ] Subscribe Continue reading Loading Comments... Write a Comment... [ ] Email [ ] Name [ ] Website [ ] [Post Comment] %d