Rozszerzenia beta-teorii rachunku lambda


16

Beta-eta-teoria rachunku lambda jest ukończona. Czy można dodać dodatkowe reguły, aby rozszerzyć teorię beta rachunku lambda, aby uzyskać teorie zbieżne inne niż teoria beta-eta?

Postscriptum

To pytanie naruszyło moją zasadę, że pytania powinny wyjaśniać, dlaczego pytający się przejmuje.

Pewnej nocy uderzyło mnie niedługo, zanim ta strona przeszła na prywatną wersję beta, ponieważ ponieważ ekstensywność i zasada wykluczonego środka są ze sobą powiązane, reguła eta jest pewnego rodzaju regułą ekstensywności, i istnieją logiki pośrednie między logiką intuicyjną a klasyczną, to byłoby interesujące, gdyby istniały takie rzeczy jak teorie „pośredniej eti”.

Gdybym to zrobił, byłoby oczywiste, że odpowiedź Evgenija rodzi oczywisty problem w sposobie, w jaki sformułowałem pytanie, zamiast być tym, o co mi chodziło.

Odpowiedzi:


8

Tak. Istnieje na przykład beta + reguła {s = t | s i t są zamkniętymi, nierozwiązywalnymi warunkami}. To, o ile pamiętam, nie jest równe beta-eta i jest spójne. Zobacz mathgate, aby uzyskać krótki opis i odniesienie do Barendregt.


To jest rzeczywiście poprawna odpowiedź na moje pytanie: beta-eta nie równa się (\ xx x) (\ xx xx) i (\ xx x) (\ x. Xx), chociaż mają to samo drzewo Böhm. Źle sformułowałem pytanie: szukam zauważalnych różnic. Prawdopodobnie powinienem to zaakceptować i zadać pytanie, które chciałem zadać ...
Charles Stewart

Zastanawiałem się nad tą odpowiedzią ... ta teoria nie jest generowana przez nowe reguły (nierozwiązywalność jest nierozstrzygalna), i nie mogę wymyślić żadnego zbieżnego zestawu reguł, który generuje podteorię tej teorii. Ale o ile wiem, może być jeden. Nowe pytanie: cstheory.stackexchange.com/questions/398/…
Charles Stewart

A moja odpowiedź na to pytanie pokazuje, że intuicja Evgenija była zdrowa, i zapewnia kombinacyjne reguły przepisywania dla jej subtheorii. Tak zaakceptowane.
Charles Stewart,
Korzystając z naszej strony potwierdzasz, że przeczytałeś(-aś) i rozumiesz nasze zasady używania plików cookie i zasady ochrony prywatności.
Licensed under cc by-sa 3.0 with attribution required.