Wiele podręczników obejmuje typy przecięć w rachunku lambda. Reguły pisania dla przecięcia można zdefiniować w następujący sposób (na górze zwykłego rachunku lambda z podtypami):
Typy skrzyżowań mają interesujące właściwości w odniesieniu do normalizacji:
- Terminarz lambda można wpisać bez użycia Iff, jeśli jest silnie normalizujący.
- Termin lambda przyjmuje typ niezawierający iff ma normalną formę.
Co jeśli zamiast dodawać skrzyżowania, dodamy związki?
Czy rachunek lambda z prostymi typami, podtypami i związkami ma jakąkolwiek interesującą podobną właściwość? Jak scharakteryzować terminy, które można wpisać w związku?
lambda-calculus
type-theory
logic
Gilles „SO- przestań być zły”
źródło
źródło
Odpowiedzi:
W pierwszym systemie to, co nazywasz subtypingiem, to dwie reguły:
Odpowiadają zasadom eliminacji dla∧ ; bez nich łącznik ∧ jest mniej lub bardziej bezużyteczny.
W drugim systemie (z łącznikami i , do którego moglibyśmy również dodać znak ) powyższe reguły podsieci są nieistotne i myślę, że towarzyszące im zasady były następujące:→ ⊥∨ → ⊥
Dla tego, co jest warte, ten system pozwala na wpisanie (przy użyciu reguły ), którego nie można wpisać tylko prostymi typami, które mają normalną formę, ale nie są silnie normalizowane .( λ x . I) Ω : A → A ⊥ E
Losowe przemyślenia: (może warto zapytać w TCS)
To prowadzi mnie do przypuszczenia, że powiązane właściwości są podobne do:
Ćwiczenie: udowodnij, że się mylę.
Wydaje się też, że jest to zdegenerowana sprawa, może powinniśmy rozważyć dodanie tego faceta do zdjęcia. O ile pamiętam, pozwoliłoby to uzyskać ?A ∨ ( A → ⊥ )
źródło
Chcę tylko wyjaśnić, dlaczego typy przecięć są odpowiednie do scharakteryzowania klas normalizacji (silna, głowa lub słaba), podczas gdy inne systemy typów nie mogą. (prosty typ lub system F).
Kluczową różnicą jest to, że musisz powiedzieć: „jeśli mogę wpisać i M 1 → M 2, to mogę wpisać M 1 ”. Często nie jest to prawdą w typach nie przecinających się, ponieważ termin można powielić:M.2) M.1→ M2) M.1
a następnie wpisanie oznacza, że możesz wpisać oba wystąpienia N, ale nie tego samego typu, na przykład M : T 1 → T 2 → T 3M.N.N. N.
Za pomocą typów skrzyżowań możesz przekształcić to w:
M : T 1 ∧ T 2 → T 1 ∧ T 2 → T 3
Teraz o typach związków: załóżmy, że możesz wpisać pomocą jakiegoś typu związku, a następnie możesz także wpisać λ x . x x, a następnie pobierz dla niektórych typów S , T 1 , … x : T 1 ∨ T 2 ∨ ⋯ ∨ T n ⊢ x x : S Ale wciąż musisz to udowodnić dla każdego i , x : T( λ x . x x ) ( λ y. y) λ x . x x S., T1, …
Dlatego nie sądzę, aby można było łatwo scharakteryzować normalizację typów związków.
źródło