Читаю Митчела, «Foundations of Programming Languages». Решаю упражнение, застопорился. Не совсем понимаю что от меня хотят.
Речь идёт о типизированном лямбда исчислении.
Exercise 1.3.2
For the purpose of this exercise and the next, the length of a typed lambda term is the number of symbols we use to write the term. For example, the length of λx:a.λy:b.y is 7. Find a pure typed lambda expression (without extra functions such as +) of the form
(λf:((a -> a) -> (a -> a)).λx:(a -> a).M) (λf:(a -> a).λx:a.f (f x))
whose length at least doubles as the result of one or more beta-reductions.
Мне нужно редуцировать приведённое выражение таким образом, чтобы его длина увеличилась вдвое, окей. Но если a в первой и второй части выражения это один и тот же тип, но похоже что здесь есть несоответствие.
второе выражение принимает два аргумента типов (a -> a) и a. Вернуть должно тоже a. То есть тип второго выражения (a -> a) -> a -> a.
В то же время первое выражение требует первый аргумент типа (a -> a) -> (a -> a).
Кроме того, правильно ли я понимаю, задание состоит в том, чтобы подобрать хитрый λ-терм заместо M?
