Eliminacja cięć dla rachunku różniczkowego lub innego typu indukcyjnego?

Czy ktoś kieruje mnie do artykułu opisującego twierdzenie o eliminacji cięć dla logiki intuicyjnej zdań, w tym indukcyjnego typu danych, takiego jak liczby naturalne (listy lub drzewa też byłyby w porządku)? Przykładem tego rodzaju systemu Jestem zainteresowany jest Gödla T, która ma typów podanych przez gramatyki . Nie bardzo interesują mnie kwantyfikatory nad liczbami naturalnymi lub predykaty indeksowane liczbami naturalnymi.$A ::= \mathbb{N} \;\;|\;\; A \to A'$

Wiem, jak udowodnić normalizację beta dla wersji tych systemów z dedukcją naturalną, używając argumentu relacji logicznych (lub powiązanych technik, takich jak NbE), ale chciałbym wiedzieć, czy istnieją standardowe odniesienia do tego, jak dostosować te metody do rachunku sekwencyjnego.

Powodem, dla którego pytam, jest to, że studiuję dodawanie operatorów stałoprzecinkowych dla strzeżonej rekurencji do języka. Idea denotacyjna jest dość stara - interpretuj typy jako przestrzenie ultrametryczne i punkty stałe za pomocą twierdzenia Banacha - ale techniki czysto syntaktyczne, które znam do udowodnienia eliminacji cięć, nie wydają się tak dobrze dostosowywać.

Co powiesz na pracę Ulricha Bergera? Na przykład Silna normalizacja zastosowanych obliczeń lambda . Część „rekurencyjnie zdefiniowane stałe” daje mniej więcej typy indukcyjne. I nie zniechęcaj się słowem „bez typu”, dostaje wyniki także dla systemów maszynowych.

Możesz rzucić okiem na McDowell i Millera Cut-Elimination dla logiki z definicjami i indukcją , która pokazuje, jak dostosować metodę Tait do intuicyjnego rachunku sekwencyjnego pierwszego rzędu z predykcyjnie zdefiniowanymi liczbami naturalnymi.