Eta expansion - name origin

Question

Just wondering where the name come from, eta?

The only two things I know about eta are:

• estimated time of arrival
• seventh letter of Greek alphabet

Answer 1

It seems that that the rules were simply taken from start of the Greek alphabet:

• α - variable renaming
• β - beta reduction
• γ - (I haven't seen any gamma rule, if you have, please let me know)
• δ - Church's delta rule (see a very short notice in Barendregt, H. P. The Lambda Calculus: Its Syntax and Semantics.):

  δ MN = T if M=N and δ MN = F if M is not N for all closed nf's M and N

• ε - (I haven't seen any epsilon rule)
• ζ - if Ux=Vx and x doesn't occur in UV then U=V
• η - the eta-rule

A further interesting source of information could be History of Lambda-calculus and Combinatory Logic by F.Cardone and J.R.Hindley, it's likely that there were some rules that have been abandoned long time ago.