Arithmetic operations in simply typed lambda calculus
Update: 2024-05-04
Description
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.
Comments
In Channel
Download from Google Play
Download from App Store
United States00:00
00:00
1.0x
