Arithmetic operations in simply typed lambda calculus

Iowa Type Theory Commute

Вміст надано Aaron Stump. Весь вміст подкастів, включаючи епізоди, графіку та описи подкастів, завантажується та надається безпосередньо компанією Aaron Stump або його партнером по платформі подкастів. Якщо ви вважаєте, що хтось використовує ваш захищений авторським правом твір без вашого дозволу, ви можете виконати процедуру, описану тут https://uk.player.fm/legal.

1+ y ago 9:56

MP3•Головна епізоду

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.

178 епізодів

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