Could you elaborate on your perception of definitions of lambda calculus? Or, say, SK calculus. They’re very simple systems and entirely syntax-directed, so I’m

Could you elaborate on your perception of definitions of lambda calculus? Or, say, SK calculus. They’re very simple systems and entirely syntax-directed, so I’m curious to know where they “go wrong”—how would you prefer a definition be presented?