Własność Churcha-Rossera dla rachunku lambda zależnie wpisanego?

Powszechnie wiadomo, że właściwość Church-Rosser obejmuje redukcję w prostym typie rachunku lambda. Oznacza to, że rachunek różniczkowy jest spójny w tym sensie, że nie wszystkie równania obejmujące terms można wyprowadzić: na przykład K I , ponieważ nie mają one tej samej postaci normalnej.λ $\beta \eta$$\lambda$$\neq$

Wiadomo również, że wynik można rozszerzyć na pary odpowiadające typom produktu.

Zastanawiam się jednak, czy można rozszerzyć wynik dla rachunku lambda zależnie wpisanego (być może) o typy polimorficzne, np. Rachunek konstrukcji?

Wszelkie referencje byłyby również świetne!

Dzięki

Przydatne może być szybkie podanie kontrprzykładu CR w kalkulacjach maszynowych za pomocą i :$\beta$$\eta$

$$t=\lambda x:A.(\lambda y:B.\ y)\ x$$

I mamy i t → r | X T : B .

$$t\rightarrow_\beta \lambda x: A.x$$ $$t\rightarrow_\eta \lambda y:B.y$$

Natychmiastowe jest, że jeśli , to dwa wynikowe warunki są w rzeczywistości równoważne, ale nie ma powodu, aby tak się działo, na warunkach nietypowych .$A\equiv B$$\alpha$

W przypadku wpisywanych terminów jest całkiem jasne, że musi być równe aby wynikowy termin był dobrze wpisany. Duża trudność, która się pojawia, jest następująca:B $A$$B$$t$

W przypadku systemów o typie zależnym należy sprawdzić konfluencję przed zachowaniem typu!

Wynika to z faktu, że potrzebujesz właściwości -injectivity w celu udowodnienia inwersji, która jest wymagana do udowodnienia zachowania / ograniczenia podmiotu.$\Pi$

$$\Pi x:A.B=_{\beta\eta}\Pi x:A'.B'\ \Leftrightarrow\ A=_{\beta\eta}A'\wedge B=_{\beta\eta} B'$$

Nie możesz więc nawet udowodnić, że zachowują typy bez zbiegu, ale zbieżność nawet nie utrzymuje niepoprawnych / źle wpisanych terminów!$\beta\eta$

Wyłamanie się z tego błędnego koła wymaga pewnych technicznych sztuczek, które trudno tutaj streścić, ale zapewne najprostszym do zrozumienia jest po prostu przestanie być zainteresowanym redukcjami, ale zamiast tego skoncentruj się na -expansions :r | T → r | * λ x : . t $\eta$$\eta$$t\rightarrow_{\eta*}\lambda x:A.t\ x$

Oczywiście, musisz ograniczyć tę regułę do terminów nie stosowanych i niestosowanych, aby nawet mieć nadzieję na zakończenie, ale z tymi ograniczeniami wydaje się, że zachowanie redukujące jest znacznie lepiej zachowane, a metaororia działa bez zbyt dużo problemów. Dobrym odniesieniem wydaje się być Neil Ghani, Eta-Expansions in The Dependent Type Theory .$\lambda$

Inne, a ostatnio dość popularne podejście, opisuje Abel, Untyped Algorytmic Equality dla Martin-Löf's Logical Framework with Surjective Pairs .

$\lambda$

• PTS z jedynie redukcją β spełniają CR na typowych warunkach. Wynika to bezpośrednio z CR dotyczących „pseudoterm”, wraz z redukcją osobników.

• Dla PTS z redukcją βη CR na zbiorze pseudoterm jest fałszywy. Zobacz (2).

• W PTS z redukcją βη CR zachowuje dobrze wpisane terminy typu stałego . Zobacz (1).

PTS są bardzo ogólnymi formalizmami i obejmują System F, Fω, LF, a także rachunek konstrukcji. Dwa ostatnie są wpisywane zależnie. Oba (1, 2) są dość starymi artykułami i wydaje mi się, że więcej wiadomo w 2015 roku.

---

^$\lambda$

^{2. RP Nederpelt, Silna normalizacja w typowanym rachunku lambda z typami strukturalnymi lambda .}