Podcasts about lambda calculus

Professor Swarat Chaudhuri from the University of Texas at Austin and visiting researcher at Google DeepMind discusses breakthroughs in AI reasoning, theorem proving, and mathematical discovery. Chaudhuri explains his groundbreaking work on COPRA (a GPT-based prover agent), shares insights on neurosymbolic approaches to AI. Professor Swarat Chaudhuri: https://www.cs.utexas.edu/~swarat/ SPONSOR MESSAGES: CentML offers competitive pricing for GenAI model deployment, with flexible options to suit a wide range of models, from small to large-scale deployments. https://centml.ai/pricing/ Tufa AI Labs is a brand new research lab in Zurich started by Benjamin Crouzier focussed on ARC and AGI, they just acquired MindsAI - the current winners of the ARC challenge. Are you interested in working on ARC, or getting involved in their events? Goto https://tufalabs.ai/ TOC: [00:00:00] 0. Introduction / CentML ad, Tufa ad 1. AI Reasoning: From Language Models to Neurosymbolic Approaches [00:02:27] 1.1 Defining Reasoning in AI [00:09:51] 1.2 Limitations of Current Language Models [00:17:22] 1.3 Neuro-symbolic Approaches and Program Synthesis [00:24:59] 1.4 COPRA and In-Context Learning for Theorem Proving [00:34:39] 1.5 Symbolic Regression and LLM-Guided Abstraction 2. AI in Mathematics: Theorem Proving and Concept Discovery [00:43:37] 2.1 AI-Assisted Theorem Proving and Proof Verification [01:01:37] 2.2 Symbolic Regression and Concept Discovery in Mathematics [01:11:57] 2.3 Scaling and Modularizing Mathematical Proofs [01:21:53] 2.4 COPRA: In-Context Learning for Formal Theorem-Proving [01:28:22] 2.5 AI-driven theorem proving and mathematical discovery 3. Formal Methods and Challenges in AI Mathematics [01:30:42] 3.1 Formal proofs, empirical predicates, and uncertainty in AI mathematics [01:34:01] 3.2 Characteristics of good theoretical computer science research [01:39:16] 3.3 LLMs in theorem generation and proving [01:42:21] 3.4 Addressing contamination and concept learning in AI systems REFS: 00:04:58 The Chinese Room Argument, https://plato.stanford.edu/entries/chinese-room/ 00:11:42 Software 2.0, https://medium.com/@karpathy/software-2-0-a64152b37c35 00:11:57 Solving Olympiad Geometry Without Human Demonstrations, https://www.nature.com/articles/s41586-023-06747-5 00:13:26 Lean, https://lean-lang.org/ 00:15:43 A General Reinforcement Learning Algorithm That Masters Chess, Shogi, and Go Through Self-Play, https://www.science.org/doi/10.1126/science.aar6404 00:19:24 DreamCoder (Ellis et al., PLDI 2021), https://arxiv.org/abs/2006.08381 00:24:37 The Lambda Calculus, https://plato.stanford.edu/entries/lambda-calculus/ 00:26:43 Neural Sketch Learning for Conditional Program Generation, https://arxiv.org/pdf/1703.05698 00:28:08 Learning Differentiable Programs With Admissible Neural Heuristics, https://arxiv.org/abs/2007.12101 00:31:03 Symbolic Regression With a Learned Concept Library (Grayeli et al., NeurIPS 2024), https://arxiv.org/abs/2409.09359 00:41:30 Formal Verification of Parallel Programs, https://dl.acm.org/doi/10.1145/360248.360251 01:00:37 Training Compute-Optimal Large Language Models, https://arxiv.org/abs/2203.15556 01:18:19 Chain-of-Thought Prompting Elicits Reasoning in Large Language Models, https://arxiv.org/abs/2201.11903 01:18:42 Draft, Sketch, and Prove: Guiding Formal Theorem Provers With Informal Proofs, https://arxiv.org/abs/2210.12283 01:19:49 Learning Formal Mathematics From Intrinsic Motivation, https://arxiv.org/pdf/2407.00695 01:20:19 An In-Context Learning Agent for Formal Theorem-Proving (Thakur et al., CoLM 2024), https://arxiv.org/pdf/2310.04353 01:23:58 Learning to Prove Theorems via Interacting With Proof Assistants, https://arxiv.org/abs/1905.09381 01:39:58 An In-Context Learning Agent for Formal Theorem-Proving (Thakur et al., CoLM 2024), https://arxiv.org/pdf/2310.04353 01:42:24 Programmatically Interpretable Reinforcement Learning (Verma et al., ICML 2018), https://arxiv.org/abs/1804.02477

It is maybe not so well known that arithmetic operations -- at least some of them -- can be implemented in simply typed lambda calculus (STLC).  Church-encoded numbers can be given the simple type (A -> A) -> A -> A, for any simple type A.  If we abbreviate that type as Nat_A, then addition and multiplication can both be typed in STLC, at type Nat_A -> Nat_A -> Nat_A.  Interestingly, things change with exponentiation, which we will consider in the next episode.

Like addition and multiplication on Church-encoded numbers, exponentiation can be assigned a type in simply typed lambda calculus (STLC).  But surprisingly, the type is non-uniform.  If we abbreviate (A -> A) -> A -> A as Nat_A, then exponentiation, which is defined as x . y . y x, can be assigned type Nat_A -> Nat_(A -> A) -> Nat_A.  The second argument needs to have type at strictly higher order than the first argument.  This has the fascinating consequence that we cannot define self-exponentiation, x . exp x x.  That term would reduce to x . x x, which is provably not typable in STLC.  

Welcome to The Nonlinear Library, where we use Text-to-Speech software to convert the best writing from the Rationalist and EA communities into audio. This is: Learning-theoretic agenda reading list, published by Vanessa Kosoy on November 9, 2023 on The AI Alignment Forum. Recently, I'm receiving more and more requests for a self-study reading list for people interested in the learning-theoretic agenda. I created a standard list for that, but before now I limited myself to sending it to individual people in private, out of some sense of perfectionism: many of the entries on the list might not be the best sources for the topics and I haven't read all of them cover to cover myself. But, at this point it seems like it's better to publish a flawed list than wait for perfection that will never come. Also, commenters are encouraged to recommend alternative sources that they consider better, if they know any. General math background "Introductory Functional Analysis with Applications" by Kreyszig (especially chapters 1, 2, 3, 4) "Computational Complexity: A Conceptual Perspective" by Goldreich (especially chapters 1, 2, 5, 10) "Probability: Theory and Examples" by Durret (especially chapters 4, 5, 6) "Elements of Information Theory" by Cover and Thomas (especially chapter 2) "Lambda-Calculus and Combinators: An Introduction" by Hindley "Game Theory: An Introduction" by Tadelis AI theory "Machine Learning: From Theory to Algorithms" by Shalev-Shwarz and Ben-David (especially part I and chapter 21) "Bandit Algorithms" by Lattimore and Szepesvari (especially parts II, III, V, VIII) Alternative/complementary: "Regret Analysis of Stochastic and Nonstochastic Multi-armed Bandit Problems" by Bubeck and Cesa-Bianchi (especially sections 1, 2, 5) "Prediction Learning and Games" by Cesa-Bianchi and Lugosi (mostly chapter 7) "Universal Artificial Intelligence" by Hutter Alternative: "A Theory of Universal Artificial Intelligence based on Algorithmic Complexity" (Hutter 2000) Bonus: "Nonparametric General Reinforcement Learning" by Jan Leike Reinforcement learning theory "Near-optimal Regret Bounds for Reinforcement Learning" (Jaksch, Ortner and Auer, 2010) "Efficient Bias-Span-Constrained Exploration-Exploitation in Reinforcement Learning" (Fruit et al, 2018) "Regret Bounds for Learning State Representations in Reinforcement Learning" (Ortner et al, 2019) "Efficient PAC Reinforcement Learning in Regular Decision Processes" (Ronca and De Giacomo, 2022) "Tight Guarantees for Interactive Decision Making with the Decision-Estimation Coefficient" (Foster, Golowich and Han, 2023) Agent foundations "Functional Decision Theory" (Yudkowsky and Soares 2017) "Embedded Agency" (Demski and Garrabrant 2019) Learning-theoretic AI alignment research agenda Overview Infra-Bayesianism sequence Bonus: podcast "Online Learning in Unknown Markov Games" (Tian et al, 2020) Infra-Bayesian physicalism Bonus: podcast Reinforcement learning with imperceptible rewards Bonus materials "Logical Induction" (Garrabrant et al, 2016) "Forecasting Using Incomplete Models" (Kosoy 2017) "Cartesian Frames" (Garrabrant, Herrman and Lopez-Wild, 2021) "Optimal Polynomial-Time Estimators" (Kosoy and Appel, 2016) "Algebraic Geometry and Statistical Learning Theory" by Watanabe Thanks for listening. To help us out with The Nonlinear Library or to learn more, please visit nonlinear.org.

It's the Season 10 finale of the Elixir Wizards podcast! José Valim, Guillaume Duboc, and Giuseppe Castagna join Wizards Owen Bickford and Dan Ivovich to dive into the prospect of types in the Elixir programming language! They break down their research on set-theoretical typing and highlight their goal of creating a type system that supports as many Elixir idioms as possible while balancing simplicity and pragmatism. José, Guillaume, and Giuseppe talk about what initially sparked this project, the challenges in bringing types to Elixir, and the benefits that the Elixir community can expect from this exciting work. Guillaume's formalization and Giuseppe's "cutting-edge research" balance José's pragmatism and "Guardian of Orthodoxy" role. Decades of theory meet the needs of a living language, with open challenges like multi-process typing ahead. They come together with a shared joy of problem-solving that will accelerate Elixir's continued growth. Key Topics Discussed in this Episode: Adding type safety to Elixir through set theoretical typing How the team chose a type system that supports as many Elixir idioms as possible Balancing simplicity and pragmatism in type system design Addressing challenges like typing maps, pattern matching, and guards The tradeoffs between Dialyzer and making types part of the core language Advantages of typing for catching bugs, documentation, and tooling The differences between typing in the Gleam programming language vs. Elixir The possibility of type inference in a set-theoretic type system The history and development of set-theoretic types over 20 years Gradual typing techniques for integrating typed and untyped code How José and Giuseppe initially connected through research papers Using types as a form of "mechanized documentation" The risks and tradeoffs of choosing syntax Cheers to another decade of Elixir! A big thanks to this season's guests and all the listeners! Links and Resources Mentioned in this Episode: Bringing Types to Elixir | Guillaume Duboc & Giuseppe Castagna | ElixirConf EU 2023 (https://youtu.be/gJJH7a2J9O8) Keynote: Celebrating the 10 Years of Elixir | José Valim | ElixirConf EU 2022 (https://youtu.be/Jf5Hsa1KOc8) OCaml industrial-strength functional programming https://ocaml.org/ ℂDuce: a language for transformation of XML documents http://www.cduce.org/ Ballerina coding language https://ballerina.io/ Luau coding language https://luau-lang.org/ Gleam type language https://gleam.run/ "The Design Principles of the Elixir Type System" (https://www.irif.fr/_media/users/gduboc/elixir-types.pdf) by G. Castagna, G. Duboc, and J. Valim "A Gradual Type System for Elixir" (https://dlnext.acm.org/doi/abs/10.1145/3427081.3427084) by M. Cassola, A. Talagorria, A. Pardo, and M. Viera "Programming with union, intersection, and negation types" (https://www.irif.fr/~gc/papers/set-theoretic-types-2022.pdf), by Giuseppe Castagna "Covariance and Contravariance: a fresh look at an old issue (a primer in advanced type systems for learning functional programmers)" (https://www.irif.fr/~gc/papers/covcon-again.pdf) by Giuseppe Castagna "A reckless introduction to Hindley-Milner type inference" (https://www.lesswrong.com/posts/vTS8K4NBSi9iyCrPo/a-reckless-introduction-to-hindley-milner-type-inference) Special Guests: Giuseppe Castagna, Guillaume Duboc, and José Valim.

Functional programming --- Send in a voice message: https://anchor.fm/david-nishimoto/message

Morgan is in the final crunch of finishing her dissertation draft, so Chris's brother Steve Webber joins us for a special "nerdout": analyzing the dual nature of fuzzy vs crisp systems! From physics to biology, from programming languages to human languages, the duality of fuzzy and crisp is everpresent.Yes, this really is what Chris and Steve sound like whenever they get together...Links:Structure and Interpretation of Computer Programs (but this version looks better on the web) and the 1980s lectures (also on Internet Archive but the YouTube uploads are more recent and higher quality)Lisp and SchemeLambda CalculusThe Little SchemerThe Most Beautiful Program Ever Written by William ByrdLisp 1.5 programmer's manual, which also now has a lovely reprint for sale (see Appendix B for Lisp in Lisp, albeit in m-expression rather than s-expression format... m-expressions never took on)Javascript: The Good PartsThe narcissism of small differencesTo Mock a Mockingbird by Raymond Smullyan. Also, presumably not the link Steve had shared with Chris back in the day (but maybe it was?) but here's a more math'y breakdown of some of the ideas, To Dissect a Mockingbird: A Graphical Notation for the Lambda Calculus with Animated ReductionDuality (mathematics)Fuzzy and crisp setsNeats and scruffies (see also our previous episode about machine learning)Alan Watts' lecture on "prickles and goo"Carcinisation (convergent evolution on "crabs")Lisp vs APL: "Mud and Diamonds"GuixJonathan Rees's websiteLojban, and here's a pretty good Lojban introThe infamous Lojban "bear goo" debate

Chris and Morgan, driving in the Covid-19 pandemic, reflect on lessons of hygiene and a separation of concerns from the past (seen through the retroactively surprising struggle for handwashing acceptance) while analyzing how to bring safety to today's computing security pandemic via object capability discipline.As said in the episode, there's a lot of research and evidence for the object capability security approach! Please do scour the links below (with significant commentary attached).Links:Ignaz Semmelweis and two excellent podcast episodes with more:Ignaz Semmelweis and the War on Handwashing on Stuff You Missed in History ClassThe fascinating, inspiring, and infurating story of Ignaz Semmelweis on SawbonesThe mailing list post by Chris that prompted this episode (largely the same stuff, a bit more particular to the targeted audience): Hygiene for a computing pandemic: separation of VCs and ocaps/zcapsPOLA Would Have Prevented the Event-Stream Incident, by Kate Sills. Examines how malicious code inserted into a library designed to steal programmers' private information/keys/money could have been prevented with capability-based security.An interview with Kate Sills about object capabilities; contains some of the same information presented in this episode, but with more focus on the basic concepts.A Security Kernel based on the Lambda Calculus explains how these concepts apply to programming language design (using a limited subset of the Scheme programming language).Ka-Ping Yee's PhD dissertation, Building Reliable Voting Machine Software, demonstrates the difficulty of finding intentionally obscured security vulnerabilities through code review (see "How was PVote's security evaluated?"). This demonstrates that FOSS is necessary but insufficient on its own for security.A backdoor which was inserted into the official Linux kernel source code (and actually distributed on the official CVS server, briefly!) all the way back in 2003. Note that the vulnerability was initially discovered not through code review, but through discovering a server intrusion. The code is well obfuscated in a way that might be difficult to observe through visual inspection of a significant body of code.The zcap-ld spec has a subsection on how to safely and hygienically bridge the worlds of identity/claims/credentials with authority/ocaps. (Note some bias here: Chris co-authored this spec with Mark Miller.) It also has some other useful subsections: Capabilities are Safer contrasts with ACLs, and ZCAP-LD by Example shows how capabilities can be constructed on top of certificate chains (an approach not even mentioned in the episode... but yes, you can do it!)So why are ACLs / an identity-oriented approach so bad anyway? ACLs Don't explains the problems caused by an identity-oriented authority model:Ambient authority, ie "programs running with too much authority"... think about the "solitaire running 'as you'" part of the podcast (and contrast with the POLA/ocap solution also explained in-episode)Confused deputies, which are notoriously kind of hard to describe... Norm Hardy provides a capsule summary which is fairly good. But also:The Browser is a very Confused Deputy is an excellent and fun video introduction.Norm Hardy's original Confused Deputy paper is still worth reading, and there is more to read hereAn example of a confused deputy attack against the Guile programming environment (which Chris helped uncover): Guile security vulnerability w/ listening on localhost + port (with fix). Note the way that both the browser and the guile programming environment appear to be "correctly behaving according to specification" when looked at individually!Another way to put it is that identity-oriented security approaches are also generally perimeter-based security approaches and (I'm paraphrasing Marc Stiegler here): "Perimeter security is eggshell security... it seems pretty tough when you tap on it, but poke one hole through and you can suck out the whole yolk."Capabilities: Effects for Free shows nicely how capabilities can also be combined with a type system to prove constraints on what a particular subset of code can do.What we haven't talked about as much yet is all the cool things that ocaps enable. A great paper on this is Capability-based Financial Instruments (aka "Ode to the Granovetter Diagram", or "The Ode"), which shows how, using the E distributed programming language, distributed financial tooling can be built out of a shockingly small amount of code. (All of this stuff written about a decade before blockchains hit the mainstream!)You might need to know a bit more E syntax to read The Ode; Marc Stiegler's E in a Walnut is an incredible resource, and has many insights of its own... but it's a bit more coconut-sized than walnut-sized, in my view.An enormous amount of interesting information and papers about object capability security on the E Wiki's Documentation page page (snapshot). Honestly you could just spend a few months reading all that.In particular, if you're mathematically minded and say "yeah but I want the proofs, gimme the proofs; I mean like real math'y proofs!" there's a whole subsection on Formal Methods (snapshot)But maybe you're worrying, is it possible to build secure UIs on top of this? Not One Click for Security does a lovely job showing how ocap principles can actually result in a more intuitive flow if done correctly... one smooth enough that users might wonder, "where's the security?" Surprise! It was just smoothly baked into the natural flow of the application, which is why you didn't notice it!And if you really want to spend a lot of time getting into the weeds of how to design ocap systems, maybe look at Mark S. Miller's PhD dissertation, Robust Composition: Towards a Unified Approach to Access Control and Concurrency Control. Chris is pretty sure they're the only one with an autographed copy sitting on their desk.Finally, have we mentioned that Chris's work on Spritely is pretty much entirely based on extending the federated social web based on ocap security principles?

Welcome to the Christmas special community edition of MLST! We discuss some recent and interesting papers from Pedro Domingos (are NNs kernel machines?), Deepmind (can NNs out-reason symbolic machines?), Anna Rodgers - When BERT Plays The Lottery, All Tickets Are Winning, Prof. Mark Bishop (even causal methods won't deliver understanding), We also cover our favourite bits from the recent Montreal AI event run by Prof. Gary Marcus (including Rich Sutton, Danny Kahneman and Christof Koch). We respond to a reader mail on Capsule networks. Then we do a deep dive into Type Theory and Lambda Calculus with community member Alex Mattick. In the final hour we discuss inductive priors and label information density with another one of our discord community members. Panel: Dr. Tim Scarfe, Yannic Kilcher, Alex Stenlake, Dr. Keith Duggar Enjoy the show and don't forget to subscribe! 00:00:00 Welcome to Christmas Special! 00:00:44 SoTa meme 00:01:30 Happy Christmas! 00:03:11 Paper -- DeepMind - Outperforming neuro-symbolic models with NNs (Ding et al) 00:08:57 What does it mean to understand? 00:17:37 Paper - Prof. Mark Bishop Artificial Intelligence is stupid and causal reasoning wont fix it 00:25:39 Paper -- Pedro Domingos - Every Model Learned by Gradient Descent Is Approximately a Kernel Machine 00:31:07 Paper - Bengio - Inductive Biases for Deep Learning of Higher-Level Cognition 00:32:54 Anna Rodgers - When BERT Plays The Lottery, All Tickets Are Winning 00:37:16 Montreal AI event - Gary Marcus on reasoning 00:40:37 Montreal AI event -- Rich Sutton on universal theory of AI 00:49:45 Montreal AI event -- Danny Kahneman, System 1 vs 2 and Generative Models ala free energy principle 01:02:57 Montreal AI event -- Christof Koch - Neuroscience is hard 01:10:55 Markus Carr -- reader letter on capsule networks 01:13:21 Alex response to Marcus Carr 01:22:06 Type theory segment -- with Alex Mattick from Discord 01:24:45 Type theory segment -- What is Type Theory 01:28:12 Type theory segment -- Difference between functional and OOP languages 01:29:03 Type theory segment -- Lambda calculus 01:30:46 Type theory segment -- Closures 01:35:05 Type theory segment -- Term rewriting (confluency and termination) 01:42:02 MType theory segment -- eta term rewritig system - Lambda Calculus 01:54:44 Type theory segment -- Types / semantics 02:06:26 Type theory segment -- Calculus of constructions 02:09:27 Type theory segment -- Homotopy type theory 02:11:02 Type theory segment -- Deep learning link 02:17:27 Jan from Discord segment -- Chrome MRU skit 02:18:56 Jan from Discord segment -- Inductive priors (with XMaster96/Jan from Discord) 02:37:59 Jan from Discord segment -- Label information density (with XMaster96/Jan from Discord) 02:55:13 Outro

In this episode we host Prof. Benjamin Delaware from Purdue University to discuss and try to answer some basic questions related to PL research: What is PL research? Why does it matter? Why is it cool? What is Lambda Calculus? What is Type Theory? Church-Turing Thesis? Curry-Howard Correspondence? What are proof assistants? Why are they cool? Don't forget to follow Ben on twitter @GhostofBendy

In this episode we host Prof. Benjamin Delaware from Purdue University to discuss and try to answer some basic questions related to PL research: What is PL research? Why does it matter? Why is it cool? What is Lambda Calculus? What is Type Theory? Church-Turing Thesis? Curry-Howard Correspondence? What are proof assistants? Why are they cool? Don't forget to follow Ben on twitter @GhostofBendy

In this episode we host Prof. Benjamin Delaware from Purdue University to discuss and try to answer some basic questions related to PL research: What is PL research? Why does it matter? Why is it cool? What is Lambda Calculus? What is Type Theory? Church-Turing Thesis? Curry-Howard Correspondence? What are proof assistants? Why are they cool? Don't forget to follow Ben on twitter @GhostofBendy

Support Topic Lords on Patreon and get episodes a week early! (https://www.patreon.com/topiclords) Lords: * Ben is not on the Internet but is just happy to be here. He recommends Lindsay Ellis, an excellent film critic: * https://www.youtube.com/channel/UCG1h-Wqjtwz7uUANw6gazRw * Ryan is The Man Who Messed Up Walking His Dog So Badly It Made The News. * http://ryannorth.ca/ * https://twitter.com/ryanqnorth Topics: * Being able to cook a recipe from your mind without being able to explain how. * Every recipe has a step called "to taste" that is a mini version of this. How much salt, pepper, chili powder and cumin do I add to these chilaquiles? I donno, it's just muscle memory. But the muscle memory only works for three eggs. More or fewer, I screw it up. * How many times a day do you remember something stupid you've done in the past? Am I normal and developing as I should? * The Ice Magic jingle in Ben’s head for the rest of his life: https://m.youtube.com/watch?v=0rfL9d4MDJY * I miss making a game that was immune to bug reports. * Dan asks: "What would we have in common with intelligent aliens? It seems common for analytical-minded people to claim that mathematical theories are discovered rather than invented. There's a programming theory personality named Phillip Wadler who's claimed that if we met aliens, they would have Lambda Calculus. Another programming personality (on the 'math is invented' side) posted a hypothetical conversation between a human programmer and an alien programmer that went like this: * Human: How do you avoid race conditions? * Alien: We just look at the different futures and pick one without data races. * Alien: How do you calm arithmetic when it's angry? * Human: Our math is not sentient." * The Atari 2600 screenshot Jim was thinking of: https://en.wikipedia.org/wiki/Arecibomessage * What's the worst thing you've ever put in your mouth? * https://en.wikipedia.org/wiki/Pacificrazorclam * Flake in Australia is a deep fried fillet of fish you can order at fish and chip shops: https://en.wikipedia.org/wiki/Flake(fish) Usually about the length of a dinner plate. * Nintendo Labo is an industrial design marvel. * Watch someone transform a Nintendo Labo keyboard into an actual synth! https://www.youtube.com/watch?v=0CjLOElL0rY * Has anyone else noticed that long-anticipated events eventually "happen" and are thereafter "in the past"? * For years my personal blog was the top internet resource for earlobe cysts. Microtopics: * Traveling to E3 from Australia. * Making games for the Nokia N-Gage. * Just now realizing that "Squirrel Girl" rhymes. * Bluffing your way through a title pun because there's limited time in a game jam. * A pun that you need to be both from England and New Zealand to get. * Procedures for recreating an unknown recipe when the recipe changes as it's observed. * A discrete series of steps that can be reproduced * A bottomless measuring cup that keeps track of how much a substance that passed through it. * A measuring cup that tells an anonymous third party you how much of a thing it holds, but doesn't tell the user. * Whether or not anything comes up if you search the internet for minestrone soup recipes. * Getting owned on Twitter after posting about the Ship of Theseus. * Feeling dumb and then later feeling dumb about how you felt dumb. * The mortifying ordeal of being known. * Dismissing intrusive thoughts with a vocal tic or a spasm. * Remembering advertising jingles from the 1980s all the goddamned time. * Whether or not the Zest jingle invented the word "zestfully" * Corporations owing serious back rent on the space in your brain taken up by advertising jingles. * Crackly choc-ice. * Going into a deep existential dread about a forty-year-old t-shirt. * Calling it the "WC" when it takes way longer to say "WC" than "water closet" * Asking the waitress where the toilet is and she gives you a weird look and says "in the bathroom, sir." * Offering your top hat for the nobleman to micturate into. * Having an audience who sees cool literary references in your work and assumes you did them on purpose. * Writing an impossible season cliffhanger believe that you're quiting the show, but then not quitting the show and having to somehow resolve the cliffhanger. * The biggest spoiler being whether or not a work is good or not. * Living vicariously through someone watching your favorite TV series for the first time. * Meeting an alien race with sentient math. * Having just the one math but being certain that it's the only math. * Doing your best to communicate with intelligent aliens but you can't think of anything to talk about. * Only trying to contact alien races that you have enough in common with to meaningfully communicate. * What kind of math a salt-leech would invent. * Coherent systems of mathematics that don't reflect reality. * Maths that would hypothetically reflect reality better than ours, and how ours could do better. * The guy waking you up from your cryogenic sleep explaining to you that we know how to divide by zero now. * Knowing that if the laws of physics change, your program will break. * Recompiling once a year to make sure your program breaks when mathematical laws are updated. * Realizing that the anecdote you're about to tell actually happened to your brother, not you. * Discovering that ants are extremely sour. * Ordering a shark kebab and the guy asks if you want crickets on it and you're certain you misheard him so you ask "what are those?" and he says "they're tiny bugs!" * Crickets just being crunchy until you look at them and realize that you're definitely eating an entire being right now. * Being stuck with your lame fish and chips when Australians have badass shark and chips. * Things you learned as a kid and never critically examined as an adult. * Razor clams: the meal that bites back. * Building a fully functional steering wheel, with levers and adjustable dials that click, out of cardboard and rubber bands. * The visual programming environment that comes with Nintendo Labo. * Buying toys for an eight year old when your son is born because one day he'll be eight. * Artisanal reprinted Nintendo Labo cardboard components on Etsy. * Taking your cardboard Nintendo Labo synth on tour and seeing how many gigs it lasts for. * Everybody really wanting to hear Jim's earlobe cyst story. * Jim's primary claim to fame before Frog Fractions. * Jim's top 3 earlobe cyst tips. * Just how deceptively close to the jugular the earlobe is. * Getting to watch a stranger's kid grow up because they don't believe you when you say they've got the wrong email address. * The kind of person who just assumes their email address is their name at gmail.com. * Holding onto the last vapors of 2012 Twitter. * Like finally talking to T-Rex.

Discussion of the basic idea of the Tait--Martin-Loef proof of confluence for untyped lambda calculus. Let me know any requests for what to discuss in Chapter 8!

Start of discussion on how to prove confluence for untyped lambda calculus. Also some discussion about the research community interested in confluence.

Adam and Jen have new jobs, they talk about complexity in the real world vs academia, and then Safia and Adam get some real-time learning in lambda calculus.

In this panel discussion, three people who knew Christopher Strachey in different contexts talk about their memories of him. Michael Jackson discusses being taught by Strachey as a boy at Harrow, David Hartley talks about work with Strachey on the programming language CPL, and Roger Penrose remembers working with Strachey at the National Research Development Corporation and introducing him to lambda calculus.

Nesse episódio nós te contamos porque você precisa saber mais de uma linguagem de programação. Aliás, muito mais que uma, ou duas ou três. Discutimos como aprender novas linguagens, os tipo de linguagem que existem, por onde começar essa caminhada, e contamos quais linguagens diferentonas nós já usamos, e quais estão na nossa pauta. Inspire-se e venha com a gente aprender linguagens novas! Feed do podcast: blog.lambda3.com.br/feed/podcast Pauta: Eu só conheço uma linguagem, e agora? Por que aprender outras linguagens? Quais linguagens já estudamos e sugerimos Quais linguagens ainda não estudamos e queremos muito estudar Linguagens e paradigmas. Estática, dinâmica, OO, funcional, etc. O que você aprendeu com uma linguagem que nunca colocou em produção? Links Citados: Curso do Eric Meyer no Channel9 sobre Haskell Livros Programação funcional através de Lambda Calculus, Greg Michaelson Seven Languages in Seven Weeks, Bruce Tate Seven More Languages in Seven Weeks, Bruce Tate Participantes: Giovanni Bassi - @giovannibassi Heber Pereira - @heberortiz Mahmoud Ali - @akamud Nicolas Takashi - @ntakashics Vinicius Quaiato - @vquaiato Créditos das músicas usadas neste programa: Music by Kevin MacLeod (incompetech.com) licensed under Creative Commons: By Attribution 3.0 – creativecommons.org/licenses/by/3.0

The Lambda Calculus uses simple replacement to compute expressions. However, it does not define a way to replace a parameter of a function with the function itself. That would seem to make it impossible to write recursive functions. However, with a clever bit of self-application, we can define a function that makes any other function recursive. This is the Y-Combinator. Claude Shannon told us that it was important to keep equivocation high in order to make a cypher difficult to crack. In the second half of his paper, he tells us how to do that. We need to diffuse the message, and we need to confuse the key. Doing these two things will destroy the statistical patterns of the message so that the only possible attack is brute force. The Two Generals problem has no solution. But does that mean that we cannot guarantee that a distributed system will reach consensus? Not at all. By applying two simplifying assumptions, we reduce the problem to one that can be solved with a very simple protocol. This durable messaging protocol guarantees that a message is received once and only once.

Claude Shannon followed up one incredibly important paper with a second of even greater significance. In Communication Theory of Secrecy Systems, he analyzes cryptosystems based on the probabilities of certain plaintext messages given an intercepted cyphertext. Understanding this form of analysis will help us to design more effective systems. The Lambda Calculus computes using nothing but symbol replacement. If we are going to run programs like a computer, we need to express conditional branches. We can represent the value "true" as a function λa.λb.a. In other words, the function that returns the first of two arguments. Similarly, the value "false" is represented by the function λa.λb.b. To create a conditional "if-else" statement, capture two branches and then apply the third argument to select between them: λa.λb.λc.c a b. Suppose that you needed to reach an agreement among several people by passing messages. Now suppose that some of those people could not be trusted. Under what conditions could you find a protocol to reach an agreement? Leslie Lamport, Robert Shostak, and Marshall Pease studied the Byzantine Generals problem to determine how to design algorithms for distributed systems.

in a translation of a paper on the Analytical Engine, Ada Lovelace improved upon L. F. Menambrea's work by applying rigor to the calculations that he performed. But then she took things one iteration further. In fact, she took things n iterations further. She wrote the first computer program, using the backtracking feature of the Analytical Engine to perform loops. The Lambda Calculus contains only functions. Evaluating a function is merely rewriting it to replace its parameter with its argument. How then can we represent something like numbers in a language with no primitives? We do it by writing a function that calls another function a certain number of times. The function that calls it once is the number 1. The function that calls it 100 times is the number 100. Alonzo Church demonstrated that these "Church Numerals" could be operated upon by other functions to calculate any computable number. We gain a great deal of confidence in our code if we can reason about the value of variables. What better way to know what a variable contains than to make sure it never changes? Immutability is not just a feature of functional programming languages. It's useful in object-oriented languages like C# and Java as well.

Top Tips For Linguists—Part I; by The SpecGram Editorial Board; From Volume CLXXIV, Number 3, of Speculative Grammarian, November 2015 — Realizing that many linguists, young and old, find themselves unsure of how best to succeed (or have success thrust upon them), we of the Speculative Grammarian Editorial Board have assembled a collection of high-impact protips that will help any linguist achieve their full potential—and then some! (Read by The SpecGram Players.)

It's Open Mic day at The Bike Shed. We hear from other thoughtbot designers and developers about what they're excited to be spending their investment time on lately. Matt Sumner Hunchpig Podcast Haskell Programming The Lambda Calculus Learn You a Haskell for Great Good Is Everyone Trying Their Best? - The Bike Shed on software quality Cole Townsend Velocity JS Cole on Dribbble The Buffalo Bills` Playoff Drought - The longest current drought in sports Joël Quenneville Alter Ego Elm Elm's Time Traveling Debugger

The Difference Engine was a mechanical computer that could calculate tables of numbers based on polynomials. The amazing thing is, though, that it could only add. How then could it accomplish this feat? By the method of differences! Charles Babbage never constructed his Difference Engine, but we've made a couple from his designs. Lambda Calculus is also a method of computation based on really simple rules. In this case, they are alpha-conversion, beta-conversion, and eta-conversion. These serious-sounding transforms are actually pretty simple. Let's first learn what they are, and then see how they relate to C#. Speaking of C#, Malachi asks a question about C# constructors. As you may know, I am of the opinion that constructor parameters should represent only immutable fields. How, then, does one initialize a mutable field in such a way that you can guarantee that it is set? In other words, write a method on the class that can only be called after the object is initialized.

Alonzo Church invented The Lambda Calculus as a simple set of rules that, when applied correctly, could compute anything that you could do with a pencil and paper. But all it is is simple replacement. Learn the basics of lambda expressions so that we can build on this theory of computation. As we celebrate pi day in the States (where we put the month in the wrong place -- 3/14/15), let's see how we go about computing the digits of pi. We'll start out with a simple geometric method, and progress through more modern techniques, until we arive at a truly surprising and remarkable formula. When John von Neumann created Game Theory, he showed how it can sometimes find an optamal strategy. But there's one game for which it fails completely. Find out why The Prisoner's Dilemma is such a tricky problem, and how a fair algorithm was found to be the best possible solution.