Let M be a λ -term, with length m, that is: m = lgh(M).
Well... I think "induction on lgh(M)" means the same as "finite induction on m". But I'm not sure.
I ask for help.
Asked
Active
Viewed 32 times
0
-
How do you define the length of a λ-term? This is not a standard notion, afaik. – sparusaurata Sep 18 '23 at 07:24
-
(a) lgh(a) = 1 for atoms a; (b) lgh(MN) = lgh(M) + lgh(N) ; (c) lgh( λx.M) = 1 + lgh(M) – Paulo Argolo Sep 18 '23 at 10:09
-
Then $\mathrm{lgh}(M)$ is the number of variables and λ's in $M$, and your induction is on this integer (induction hypothesis: the property is true for all $M'$ with fewer variables and λ's). “Induction on $M$” would be a structural induction, on the top-level constructor of $M$ (induction hypothesis: the property is true for all strict subterm of $M$). – sparusaurata Sep 18 '23 at 12:57