The curious case of exponentiation in simply typed lambda calculus

Iowa Type Theory Commute

#Science #Tech #Math #Aaron Stump #Programming Language #Computational Logic #Type Theory #Proof Assistants #Cedille

1:03:38

Too many entrepreneurs get stuck on the business treadmill, hustling nonstop, unable to scale, and unknowingly stalling their growth. That’s where Dave Ramsey began. After crashing into $3 million in debt, he rebuilt from scratch, turning a small radio program into a national show with millions of listeners. With over three decades of experience in entrepreneurship, business growth, and content creation, he knows what it takes to build a lasting business. In this episode, Dave reveals the six drivers of long-term success, the five key stages of startup growth, and how he balances life as an entrepreneur and a content creator. In this episode, Hala and Dave will discuss: (00:00) Introduction (00:23) The Core Principles of Financial Freedom (05:42) Adapting to Change as a Content Creator (09:22) Balancing Content Creation and Entrepreneurship (12:34) How to Create a Clear Path in Business (15:19) The Truth About Starting a Business Today (18:22) The Six Drivers of Business Success (26:20) Shifting From Tactical to Strategic Thinking (29:44) The Five Stages of Business Growth (41:10) Leading with Care, Clarity, and Accountability (47:10) Identifying the Right Leadership Skills (48:35) Starting a Media Business as an Entrepreneur Dave Ramsey is a personal finance expert, radio personality, bestselling author, and the founder and CEO of Ramsey Solutions. Over the past three decades, he has built a legacy of helping millions achieve financial freedom. As the host of The Ramsey Show , Dave reaches more than 18 million listeners each week. He is the author of eight national bestselling books. His latest, Build a Business You Love , helps entrepreneurs navigate growth and overcome challenges at every stage. Sponsored By: Shopify - Sign up for a one-dollar-per-month trial period at youngandprofiting.co/shopify OpenPhone: Streamline and scale your customer communications with OpenPhone. Get 20% off your first 6 months at openphone.com/profiting Airbnb - Find yourself a co-host at airbnb.com/host Indeed - Get a $75 sponsored job credit at indeed.com/profiting RobinHood - Receive your 3% boost on annual IRA contributions, sign up at robinhood.com/gold Factor - Get 50% off your first box plus free shipping at factormeals.com/factorpodcast Rakuten - Save while shopping at rakuten.com Microsoft Teams - Stop paying for tools. Get everything you need, for free at aka.ms/profiting LinkedIn Marketing Solutions - Get a $100 credit on your next campaign at linkedin.com/profiting Resources Mentioned: Dave’s Book, Build a Business You Love: bit.ly/BuildaBusinessYouLove Dave’s Website: ramseysolutions.com Active Deals - youngandprofiting.com/deals Key YAP Links Reviews - ratethispodcast.com/yap Youtube - youtube.com/c/YoungandProfiting LinkedIn - linkedin.com/in/htaha/ Instagram - instagram.com/yapwithhala/ Social + Podcast Services: yapmedia.com Transcripts - youngandprofiting.com/episodes-new Entrepreneurship, Entrepreneurship Podcast, Business, Business Podcast, Self Improvement, Self-Improvement, Personal Development, Starting a Business, Strategy, Investing, Sales, Selling, Psychology, Productivity, Entrepreneurs, AI, Artificial Intelligence, Technology, Marketing, Negotiation, Money, Finance, Side Hustle, Mental Health, Career, Leadership, Mindset, Health, Growth Mindset, Side Hustle, Passive Income, Online Business, Solopreneur, Networking.…

for ca. et år siden 7:29

MP3•Episode hjem

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.

173 episoder

The curious case of exponentiation in simply typed lambda calculus

Iowa Type Theory Commute

17 subscribers

published for ca. et år siden

Del

MP3•Episode hjem

173 episoder

#Science #Tech #Math #Aaron Stump #Programming Language #Computational Logic #Type Theory #Proof Assistants #Cedille

Alle episoder

1
A Measure-Based Proof of Finite Developments 23:24

for 2 dage siden23:24

23:24

I discuss the paper "A Direct Proof of the Finite Developments Theorem" , by Roel de Vrijer. See also the write-up at my blog.

1
Introduction to the Finite Developments Theorem 15:54

for 22 dage siden15:54

15:54

The finite developments theorem in pure lambda calculus says that if you select as set of redexes in a lambda term and reduce only those and their residuals (redexes that can be traced back as existing in the original set), then this process will always terminate. In this episode, I discuss the theorem and why I got interested in it.…

1
Nominal Isabelle/HOL 16:18

for 11 weeks siden16:18

16:18

In this episode, I discuss the paper Nominal Techniques in Isabelle/HOL , by Christian Urban. This paper shows how to reason with terms modulo alpha-equivalence, using ideas from nominal logic. The basic idea is that instead of renamings, one works with permutations of names.

1
The Locally Nameless Representation 19:54

for 15 weeks siden19:54

19:54

I discuss what is called the locally nameless representation of syntax with binders, following the first couple of sections of the very nicely written paper "The Locally Nameless Representation," by Charguéraud. I complain due to the statement in the paper that "the theory of λ-calculus identifies terms that are α-equivalent," which is simply not true if one is considering lambda calculus as defined by Church, where renaming is an explicit reduction step, on a par with beta-reduction. I also answer a listener's question about what "computational type theory" means. Feel free to email me any time at aaron.stump@bc.edu, or join the Telegram group for the podcast.…

1
POPLmark Reloaded, Part 1 15:14

for 17 weeks siden15:14

15:14

I discuss the paper POPLmark Reloaded: Mechanizing Proofs by Logical Relations , which proposes a benchmark problem for mechanizing Programming Language theory.

1
POPLmark Reloaded, Part 2 13:59

for 17 weeks siden13:59

13:59

I continue the discussion of POPLmark Reloaded , discussing the solutions proposed to the benchmark problem. The solutions are in the Beluga, Coq (recently renamed Rocq), and Agda provers.

1
Introduction to Formalizing Programming Languages Theory 12:20

for 21 weeks siden12:20

12:20

In this episode, I begin discussing the question and history of formalizing results in Programming Languages Theory using interactive theorem provers like Rocq (formerly Coq) and Agda.

1
Turing's proof of normalization for STLC 17:39

for 48 weeks siden17:39

17:39

In this episode, I describe the first proof of normalization for STLC, written by Alan Turing in the 1940s. See this short note for Turing's original proof and some historical comments.

1
Introduction to normalization for STLC 9:39

for 49 weeks siden9:39

9:39

In this episode, after a quick review of the preceding couple, I discuss the property of normalization for STLC, and talk a bit about proof methods. We will look at proofs in more detail in the coming episodes. Feel free to join the Telegram group for the podcast if you want to discuss anything (or just email me at aaron.stump@gmail.com).…

1
Arithmetic operations in simply typed lambda calculus 9:56

for 50 weeks siden9:56

9:56

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.…

1
The curious case of exponentiation in simply typed lambda calculus 7:29

for 50 weeks siden7:29

7:29

1
More on basics of simple types 15:45

for 51 weeks siden15:45

15:45

I review the typing rules and some basic examples for STLC. I also remind listeners of the Curry-Howard isomorphism for STLC.

1
Begin Chapter on Simple Type Theory 15:41

for 52 weeks siden15:41

15:41

In this episode, after a pretty long hiatus, I start a new chapter on simply typed lambda calculus. I present the typing rules and give some basic examples. Subsequent episodes will discuss various interesting nuances...

1
Some advanced examples in DCS 23:16

for 2 years siden23:16

23:16

This episode presents two somewhat more advanced examples in DCS. They are Harper's continuation-based regular-expression matcher, and Bird's quickmin, which finds the least natural number not in a given list of distinct natural numbers, in linear time. I explain these examples in detail and then discuss how they are implemented in DCS, which ensures that they are terminating on all inputs.…

1
DCS compared to termination checkers for type theories 19:45

for 2 years siden19:45