Charakterystyka terminów lambda, które mają typy związków

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):

\frac{Γ ⊢ M. : {T.}_{1} Γ ⊢ M. : {T.}_{2)}}{Γ ⊢ M. : {T.}_{1} \land {T.}_{2)}} (\land ja) \frac{}{Γ ⊢ M. : ⊤} (⊤ ja)

$\dfrac{\Gamma \vdash M : T_1 \quad \Gamma \vdash M : T_2} {\Gamma \vdash M : T_1 \wedge T_2} (\wedge I) \qquad\qquad \dfrac{} {\Gamma \vdash M : \top} (\top I)$

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. $\top I$
Termin lambda przyjmuje typ niezawierający iff ma normalną formę. $\top$

Co jeśli zamiast dodawać skrzyżowania, dodamy związki?

\frac{Γ ⊢ M : T_{1}}{Γ ⊢ M : T_{1} \lor T_{2}} (\lor I_{1}) \frac{Γ ⊢ M : T_{2}}{Γ ⊢ M : T_{1} \lor T_{2}} (\lor I_{2})

$\dfrac{\Gamma \vdash M : T_1} {\Gamma \vdash M : T_1 \vee T_2} (\vee I_1) \qquad\qquad \dfrac{\Gamma \vdash M : T_2} {\Gamma \vdash M : T_1 \vee T_2} (\vee I_2)$

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

Interesujące pytanie. Czy możesz powiedzieć, że interfejsy OOP odpowiadają temu?

— Raphael

Może możesz zainteresować się tym cs.cmu.edu/~rwh/courses/refinements/papers/Barbaneraetal95/…

— Fabio F.

Odpowiedzi:

W pierwszym systemie to, co nazywasz subtypingiem, to dwie reguły:

\frac{Γ, x : T_{1} ⊢ M : S}{Γ, x : T_{1} \land T_{2} ⊢ M : S} (\land E_{1}) \frac{Γ, x : T_{2} ⊢ M : S}{Γ, x : T_{1} \land T_{2} ⊢ M : S} (\land E_{2})

$\dfrac{Γ, x:T_1 \vdash M:S}{Γ, x:T_1 ∧ T_2 \vdash M:S}(∧E_1)\quad\dfrac{Γ, x:T_2 \vdash M:S}{Γ, x:T_1 ∧ T_2 \vdash M:S}(∧E_2)$

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: $∨$ $→$ $⊥$

\frac{Γ, x : T_{1} ⊢ M : S Γ, x : T_{2} ⊢ M : S}{Γ, x : T_{1} \lor T_{2} ⊢ M : S} (\lor E) \frac{}{Γ, x : ⊥ ⊢ M : S} (⊥ E)

$\dfrac{Γ, x: T_1 \vdash M:S\quad Γ, x:T_2 \vdash M:S}{Γ, x:T_1 ∨ T_2 \vdash M:S}(∨E)\quad\dfrac{}{Γ, x: {⊥} \vdash M:S}({⊥}E)$

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:

λ-termin przyjmuje typ niezawierający iff ma postać normalną dla wszystkich które mają postać normalną. ( nie przejdzie obu testów, ale powyższy λ-termin je zalicza) $M$ $⊥$ $MN$ $N$ $δ$
λ okresie mogą być drukowane bez użycia zasada IFF jest silnie normalizację dla każdego silnie normalizowania . $M$ ${⊥}E$ $MN$ $N$

Ć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 → {⊥})$

— Stéphane Gimenez
źródło

Dobra uwaga na temat reguł podsieci, pokazują, że typy unii nie są tak naturalne jak przecięcia (które są wpisywane prostopadle do strzałek). O drugiej części muszę jeszcze trochę pomyśleć.

— Gilles 'SO - przestań być zły'

Myślę, że

odpowiada na ćwiczenie, jeśli mówimy o typach związków.

M = (λ x . x x) (λ y . y)

$M=(\lambda x.xx)(\lambda y.y)$

— jmad

O call / cc: potrzebuje więcej niż tylko warunków lambda (takich jak lambda-mu lub inne ramy), ale systemy typów są bardziej złożonymi, logicznymi systemami, w których typy związków mogą być nieistotne.

— jmad

@jmad: Rzeczywiście, do wpisania tego terminu potrzebne są typy skrzyżowań :-( Może rozważenie związków i skrzyżowań razem byłoby interesujące?

— Stéphane Gimenez

Byłbym zainteresowany λ-terminem, który można pisać z typami unii (rs. Z typami przecięcia), ale nie z typami prostymi (rs. Z typami przecięcia).

— jmad

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 to mogę wpisać ”. Często nie jest to prawdą w typach nie przecinających się, ponieważ termin można powielić: $M_2$ $M_1→M_2$ $M_1$

(λ x . M. x x) N. \to M. N. N.

$(\lambda x.Mxx)N → MNN$

a następnie wpisanie oznacza, że możesz wpisać oba wystąpienia ale nie tego samego typu, na przykład $MNN$ $N$ Za pomocą typów skrzyżowań możesz przekształcić to w:

M. : {T.}_{1} \to {T.}_{2)} \to {T.}_{3)} N. : {T.}_{1} N. : {T.}_{2)}

$M:T_1→T_2→T_3 \qquad N:T_1 \qquad N:T_2$

a następnie kluczowy krok jest teraz naprawdę łatwy:

M. : {T.}_{1} \land {T.}_{2)} \to {T.}_{1} \land {T.}_{2)} \to {T.}_{3)} N. : {T.}_{1} \land {T.}_{2)}

$M:T_1\wedge T_2→T_1\wedge T_2→T_3 \qquad N:T_1\wedge T_2$

można wpisywać za pomocą typów przecięć.

(λ x . M. x x) : {T.}_{1} \land {T.}_{2)} \to {T.}_{3)} N. : {T.}_{1} \land {T.}_{2)}

$(\lambda x.Mxx):T_1\wedge T_2→T_3 \qquad N:T_1\wedge T_2$

(λ x . M x x) N

$(\lambda x.Mxx)N$

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ć a następnie pobierz dla niektórych typów Ale wciąż musisz to udowodnić dla każdego , $(\lambda x.xx)(\lambda y.y)$ $\lambda x.xx$ $S, T_1, \dots$

x : {T.}_{1} \lor {T.}_{2)} \lor \dots \lor {T.}_{n} ⊢ x x : S.

$x : T_1\vee T_2 \vee \dots \vee T_n ⊢xx:S$

i

$i$

co wydaje się niemożliwe, nawet jeśli

jest rodzajem związku.

x : T_{i} ⊢ x x : S

$x:T_i⊢xx:S$

S

$S$

Dlatego nie sądzę, aby można było łatwo scharakteryzować normalizację typów związków.

— jmad
źródło