Czy istnieją pośrednie teorie eta dla rachunku lambda?

Istnieją dwie główne, zbadane teorie rachunku lambda, teorii beta i jej rozwinięcia post-zupełnego, teorii beta-eta.

Czy te dwie teorie mają pośrednią, rodzaj pośredniej reguły eta, która daje spójną teorię przepisywania? Czy istnieje jakieś interesujące pojęcie częściowej ekstensywności, któremu ono odpowiada?

Jest to drugie pytanie, które zadałem w ramach pośredniej eta, przy czym poprzednie było rozszerzeniem beta-teorii rachunku lambda , co doprowadziło do pytania o ortogonalne pojęcie rozszerzenia, charakteryzujące niewidzialne równoważności poprzez zbieżne reguły przepisywania , które miały na celu wyjaśnienie odpowiedz na to wcześniejsze pytanie.

W przypadku kalkulatorów maszynowych, jeśli weźmiesz pod uwagę typy ujemne ( , × , → ), możesz włączać i wyłączać reguły eta praktycznie w dowolnym momencie, bez wpływu na zbieżność.$1$$\times$$\to$

W przypadku typów dodatnich (sum i par z eliminacją dopasowania do wzorca) sytuacja jest znacznie bardziej chaotyczna. Zasadniczo pytanie brzmi, czy termin ma formę eliminacji o zamkniętym zakresie, która pozwala kontekstom na interakcję w skomplikowany sposób z rozszerzeniem eta. Na przykład, jeśli ma typ A × B , to jego eta-ekspansja jest l e $e$$A \times B$ . Ale aby uzyskać teorię równań, której oczekiwałby teoretyk kategorii, należy wziąć pod uwagę konteksty C [ - ] i uogólnić równanie na C [ e ] ≡ l e $\mathsf{let}\;(a,b) = e \;\mathsf{in}\; (a,b)$$\mathbb{C}[-]$ (z oczekiwanymi ograniczeniami zakresu).$\mathbb{C}[e] \equiv \mathsf{let}\;(a,b) = e\;\mathsf{in}\;\mathbb{C}[(a,b)]$

Myślę, że nadal możesz udowodnić wynik zbiegu, jeśli nie zezwolisz na konwersję dojazdów do pracy. Ale to jest pogłoska - sam nigdy tego nie próbowałem ani nie przeglądałem dokumentów dokumentujących to.

Ale tak naprawdę nie wiem nic o nietypowym rachunku lambda.

EDYCJA: Charles pyta o eta-redukcje. Jest to obiecujące dla tego rodzaju przykładu, którego szuka, ponieważ myślę, że ogólnie nie będą one wystarczająco silne, aby modelować pełną teorię równości, którą zilustruję prostym przykładem obejmującym booleany. Ekspansja eta dla booleanów to . (Redukcja eta jest oczywiście w innym kierunku).$\mathbb{C}[e] \mapsto \mathsf{if}(e, \mathbb{C}[\mathsf{true}], \mathbb{C}[\mathsf{false}])$

Teraz rozważmy termin . Wskazując, że termin ten jest równoważny z i f ( e , $\mathsf{if}(e, f, g)\;\mathsf{if}(e, x, y)$ musi przejść przez eta spieniania, ponieważ trzeba wymienić e w jednym z jeżeli-to-elses połączeniu z t r ù e and f danego ł s e w celu doprowadzenia do p -redukcja. $\mathsf{if}(e, f\;x, g\;y)$$e$$\mathsf{true}$$\mathsf{false}$$\beta$

Według Johna C. Mitchella w Foundations of Programming Languages, zarówno w STLC, jak i w niepisanym rachunku lambda, reguła redukcji pair (proj₁ P, proj₂ P) → Pprzerywa konfluencję w połączeniu z fixredukcją (lub, jak przypuszczam, patrząc na dowód), bez takich warunków dla nietypowego przypadku. To jest twierdzenie 4.4.19 (strona 272).