Лямбда-исчисление и аксиоматика Пеано

[nikov]

Очень нужна информация о том, как можно выразить утверждения о лямбда-термах на языке арифметики Пеано. В частности, как перевести на язык АП утверждения "нормальная редукция такого-то лямбда терма никогда не завершается" или "нормальная редукция такого-то лямбда терма завершается через N шагов"?
Спасибо.

[Мастак]

То есть надо записывать выражения без функциональных символов (лямбда-исчисление)?
Были статьи, где сопоставляли арифметику Пеано и машину Тьюринга, записывая вычисления на машине Тьюринга и потом отображая это на языке арифметики Пеано.