reductions

Stream: maths

[Kenny Lau]

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

[Andrew Ashworth]

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

[Andrew Ashworth]

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

[Andrew Ashworth]

ncatlab has the rest

[Kenny Lau]

ncatlab :o

[Andrew Ashworth]

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]

i didn't say i don't like ncatlab

[Andrew Ashworth]

heh, cross out my 'too' then

[Mario Carneiro]

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

[Mario Carneiro]

delta is definition reduction, replace a definition with its definiens

[Mario Carneiro]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Mario Carneiro]

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