Brady Haran interview with Terence Tao

He's talking about the New New Math:


My comment:

9:47 He's analogous to a Category Theorist then?

Douglas Hofstadter too, see What is Formal Logic? 

Subscribe to Numberphile.

See Brady Haran Interview with Hugo Duminil-Copin.

Andrej Bauer just gave a lecture to his students on Arithmetic of Sets, or Cartesian Closed Categories or something. I'm sure students would be much less put off by logarithms if they learned this first, ... See Logic and Sets by Andrej Bauer and Davorin Lešnik. 

 

The name of the game is to explain this oft-commented-upon wrinkle in Arithmetic:

In other words, why is 0⁰=1? I mean 0¹=0 so why is a higher exponent less than a lower one?

I remember the first time I tried to use higher-order functors in Moscow ML, I wrote a functor which took a pair of functors as an argument and somehow applied the first one to the second. It was something like a successor function and a zero element, but completely abstract.

It was based on this:

Then just to try it out I started with simplest arguments which were the arithmetic successor function and the arithmetic zero, and I looked at the result of iterating this twice. It produced a table of exponents, and when I teased apart what it had done in terms of lambda expressions I found I had a really interesting definition of a ternary arithmetic operator whose first argument was an iteration level and whose other two arguments were the arguments to addition, multiplication and exponentiation, but with a subtle swapping of the roles of the arguments on the way down. See MSP Strathclyde Lecture - Conor McBride on Bi-directional Typing and the discipline of mechanism.  It was interesting, and I guess you can do something like this with Cartesian Closed Categories. It seemed to be something more than primitive recursion. By the Curry-Howard correspondence these structures are all formal proofs in some sense. See 50 Years of the Roche Biochemical Pathways Poster.

Google AI gave me a half-intelligent answer when I asked "What is the most concise theory exhibiting the isomorphism in set theory between Cartesian product and disjoint sum and arithmetic addition, multiplication and exponentiation?"

See Robert Atkey - Containers and this 2013 paper Categories within the Foundation of Mathematics by Benjamin Horowitz.

Subscribe to Andrej Bauer. 

Comments

Post a Comment

Popular posts from this blog

John Searle's Chinese Room Argument

Image
He's fed up with talking about this. I used to have a copy of the little book he wrote called Minds, Brains & Science. Apparently the AI at Google has read it too and gets it completely: How does stuff like this happen? Most people won't even notice what I'm saying even if I point out that the Google search changed the title. The book was really called Minds, Brains & Science , not Minds, Brains & Programs . (But maybe that was a later edition or something?) I asked Google and it said: John Searle's book Minds, Brains and Science did not become "Minds, Brains & Programs"—rather, they are two separate, distinct works published a few years apart: "Minds, Brains, and Programs" (1980): A landmark academic paper published in the journal Behavioral and Brain Sciences. This is where Searle first introduced his famous Chinese Room Argument to challenge the concept of "strong AI". "Minds, Brains and Science" (1984): A shor...
Read more

Tensor Fields and Simplicial Complexes

Image
Listening to Freya Holmér last night I started to get glimmers of an idea I had long ago about how to represent vector spaces in computational processes using this recursive abstract type :  abstype 'a point = POINT   of {getx :  'a vector,       diff :  'a point -> 'a point,       move :  'a point -> 'a point,       scale : 'a -> 'a point,       proj :  'a point -> 'a} with    fun new i (op +) (op -) (op * ) dot =    let fun self x =  POINT       {getx = x,        move = fn (POINT pr) =>           (self (x + (#getx pr))),        diff = fn (POINT pr) =>          self (x - (#getx pr)),        scale = fn i =>          (self (x * i)),        proj = fn (POINT pr) =>     ...
Read more

FUTO FUBS

Image
I think this is the first time they've actually publicly announced anything about this project. See these posts: Eron Woolf on Why Open Source is Failing Matt Mikhailov and Vincent McKibbon on The Problem with Open Hardware Jason Kridner talking About BeagleBoard.org and Software Development .  See these places:  https://danielc.dev/rk/ https://github.com/petabyt/rk https://github.com/futo-org/ret See also  https://pine64.org/devices/pinebook_pro/ . Subscribe to  FUTO .  See  https://github.com/nir9/low-level-learning-resources/tree/master/setups/debian . Subscribe to  Nir Lichtman .  If you're looking for a cool init process, try  https://ctx.graphics/terminal/ . See  Artful Bytes - When to Use a RTOS  and  How to Create a Successful Open Source Project . 
Read more