## Stream: maths

### Topic: reductions

#### Kenny Lau (May 27 2018 at 22:30):

What are alpha, beta, delta, zeta, eta, iota reudctions?

#### Andrew Ashworth (May 27 2018 at 22:32):

http://www.aplusplus.net/lcintro.pdf

#### Andrew Ashworth (May 27 2018 at 22:32):

it might not have some of the fancier reductions, but its got the basics

#### Andrew Ashworth (May 27 2018 at 22:33):

ncatlab has the rest

ncatlab :o

#### Andrew Ashworth (May 27 2018 at 22:34):

i, too, dislike going to ncatlab first, but for some reason the people there really like dtt and hott and so they have a decent encyclopedia of concepts

#### Kenny Lau (May 27 2018 at 22:35):

i didn't say i don't like ncatlab

#### Andrew Ashworth (May 27 2018 at 22:35):

heh, cross out my 'too' then

#### Mario Carneiro (May 27 2018 at 22:40):

the lambda calculus has alpha, beta, eta, and they have the same meaning in DTT

#### Mario Carneiro (May 27 2018 at 22:40):

delta is definition reduction, replace a definition with its definiens

#### Mario Carneiro (May 27 2018 at 22:40):

zeta is let reduction, let x := t in s -> s[t/x]

#### Mario Carneiro (May 27 2018 at 22:41):

iota is for inductive types, a T.rec where the major premise is a constructor of the type

#### Mario Carneiro (May 27 2018 at 22:42):

actually alpha is not a reduction, and eta is not usually used as a reduction either, they are just equalities

#### Mario Carneiro (May 27 2018 at 22:42):

and alpha isn't even needed in lean because de bruijn indices make alpha equivalent expressions syntactically equal

Last updated: May 19 2021 at 03:22 UTC