Zulip Chat Archive

Stream: maths

Topic: reductions


view this post on Zulip Kenny Lau (May 27 2018 at 22:30):

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

view this post on Zulip Andrew Ashworth (May 27 2018 at 22:32):

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

view this post on Zulip Andrew Ashworth (May 27 2018 at 22:32):

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

view this post on Zulip Andrew Ashworth (May 27 2018 at 22:33):

ncatlab has the rest

view this post on Zulip Kenny Lau (May 27 2018 at 22:33):

ncatlab :o

view this post on Zulip 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

view this post on Zulip Kenny Lau (May 27 2018 at 22:35):

i didn't say i don't like ncatlab

view this post on Zulip Andrew Ashworth (May 27 2018 at 22:35):

heh, cross out my 'too' then

view this post on Zulip Mario Carneiro (May 27 2018 at 22:40):

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

view this post on Zulip Mario Carneiro (May 27 2018 at 22:40):

delta is definition reduction, replace a definition with its definiens

view this post on Zulip Mario Carneiro (May 27 2018 at 22:40):

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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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