(no subject)

[66george]

А вот такая мысль пришла. Допустим, мы определяем функцию на лямбда-термах "количество лямбд, идущих в линию"
rang : Lambda -> nat
rang(x) = 0
rang(lambda x M) = rang(M) + 1
rang(MN) = max(rang(M), rang(N))
Введём два семейства множеств
A(n) = {M | rang(M) = n}
B(n) = {M | rang(M) < n}
Тогда их можно определить как индуктивные типы
B(0) = пустое множество
B(n+1) = B(n) + A(n)
то есть B(n+1) = A(0) +...+ A(n)
A(0) = Var + A(0)xA(0)
то есть терм M из A(0) есть либо переменная, либо аппликация двух термов из A(0)
A(n+1) = VarxA(n) + A(n+1)xA(n+1) + A(n+1)xB(n+1) + B(n+1)xA(n+1)
то есть терм M из A(n+1) либо имеет вид lambda z N, где N из A(n), либо является аппликацией двух термов, хотя бы один из которых принадлежит A(n+1) (имеет ранг n+1), а второй имеет ранг n+1 или меньше.
Тогда Lambda = Summa (n) A(n)
Дальше, мы определяем подстановку [N/x]M не как функцию
[] : LambdaxVarxLambda -> Lambda
а как функцию
[]_n : LambdaxVarxA(n) -> Lambda
то есть считаем, что M принадлежит A(n)
При определении подстановки проблемный пункт выглядит так
[N/x] lambda y M = lambda z [N/x] [z/y] M
где переменная z "свежая". Тут непонятно, по чему рекурсия. [z/y] M не является подтермом lambda y M
Но оно имеет ранг на единицу меньше, одна лямбда пропала! И мы можем определить подстановку индукцией по рангу и пытаться доказать её свойства тоже индукцией по рангу. И тут же выписал определения в Coq и Coq их не принимает, выдавая странные ошибки. Поискал на форумах -- это не моя проблема, это проблема Coq. Он "умеет работать с зависимыми типами" весьма относительно.
P.S. Как жаль, что Куклев после десятого бустера превратился в двуногую бациллу.