Literówka w rachunku papieru konstrukcyjnego?

10

W klasycznym rachunku papierów konstrukcyjnych istnieje reguła, która stwierdza

wprowadź opis zdjęcia tutaj (strona 7 pdf, strona 101 oryginalnego dokumentu)

Zasada ta oznaczałaby, że każdy kontekst można zredukować do członka tego kontekstu. Wydaje się, że nie powinno to być poprawne, ponieważ pociągałoby za sobą

1 ≅ Nat
3 ≅ Nat
1 ≅ 3

jeśli Nat jest kontekstem.

Myślę, że najlepszą interpretacją jest to, że dolna delta miała być M. Szczególnie biorąc pod uwagę zasady podane na następnej stronie.

Czy to po prostu literówka, czy jakaś subtelna logiczna zasada, której nie rozumiem?

lo.logic calculus-of-constructions sequent-calculus użytkownik833970
źródło

Odpowiedzi:

11

Γ⊢M:ΔΓ⊢M≅M

Γ⊢N≅M

Nieco intuicyjnie dowodzenie, że system z konwersją typów jest równoważny z systemem bez typów, jest bardzo trudne i zostało rozstrzygnięte w 2010 r. Przez Silesa i Herbelina .

cody
źródło
„Nowoczesne zabiegi” oznaczają tutaj „komputerowe zabiegi naukowe najbardziej zainteresowane obliczeniami”.
Andrej Bauer,
Słusznie. Prawie wychowałem szkoły teorii typu „szwedzkie” vs. „francuskie”, ale nie jestem pewien, czy rzeczywiście istnieje takie rozróżnienie.
cody
Nie ma takiego rozróżnienia, o czym świadczy fakt, że Thierry Coquand mieszka w Szwecji. Wszystkie są obliczeniowe.
Andrej Bauer,
@cody: Myślałem, że prawie wszystkie współczesne, komputerowe nauki wykorzystują maszynopisane sądy, ponieważ jest to najwygodniejszy sposób na uzyskanie eta dla pi / sigma. (Z pewnością Coq i Agda popierają to.)
Neel Krishnaswami,
@NeelKrishnaswami Konwersja na maszynie jest niezbędna, aby eta miała sens w większości sytuacji, ale miałem wrażenie, że może to uczynić meta-teorię znacznie trudniejszą. Może się całkowicie mylę i to naprawdę wszystko upraszcza. Istnieje również kwestia optymalizacji kontroli konwersji, aby wykonać jak najmniej pracy, w tym dodatkowych obowiązków związanych z kontrolą typu. Z pewnością byłoby to świetne pytanie uzupełniające.
cody