Sistema dei Tipi

Question 1

Regole di inferenza F1: applicazione MN

Answer 1

Γ⊢M:A→B Γ⊢N:A
​Γ⊢MN:B

Applicando una “funzione” di tipo A → B ad un “argomento” del giusto tipo A, si ottiene un “risultato” di tipo B.

Question 2

Regole di inferenza F1: costanti

Answer 2

Γ⊢k:K

Question 3

Regole di inferenza F1: variabili

Answer 3

Γ₁ (x:A),Γ ₂⊢x:A

Question 4

Regole di inferenza F1: lambda astrazioni

Answer 4

Γ( x : A )⊢ M : B
Γ ⊢ fn x : A.M : A → B

Consente di assegnare un tipo
freccia A → B a termini della forma λ x : A . M (chiamati lambda-astrazioni) in
un contesto Γ

Question 5

Cosa vuol dire “astrarre su un tipo”?

Answer 5

Nel sistema F1 (prim’ordine) i termini vengono tipati in un contesto dei tipi: il judgement
x : int ⊢x+ 1 : int asserisce che x+ 1 è un termine legale di tipo int nel contesto che assegna il tipo int alla variabile x.
In un sistema dei tipi del second’ordine
le variabili agiscono da segnaposto non solo per i termini, ma anche per i tipi.
E dunque possibile scrivere un tipo come X → int in cui la variabile X segna il
posto per un tipo arbitrario.

Question 6

Regole di inferenza F2: Λ X .M

Answer 6

Γ ⊢ M : A
Γ ⊢ Λ X . M : ∀X . A
(se X not∈ free(Γ))

Question 7

Regole di inferenza F2: MB

Answer 7

Γ ⊢ M : ∀ X . A
Γ ⊢ M B : [B/X] A

Question 8

Regole di inferenza Fun_τ: x

Answer 8

Γ1, x : σ, Γ2 ⊢ x : σ

Question 9

Regole di inferenza Fun_τ: M se (σ > σ’)

Answer 9

Γ ⊢ M : σ
Γ ⊢ M : σ’
(σ > σ’)

Question 10

Regole di inferenza Fun_τ: M se X not∈ free (Γ)

Answer 10

Γ ⊢ M : σ
Γ ⊢ M : ∀X . σ

(X not ∈ free (Γ))

Question 11

Regole di inferenza Fun_τ: let x = M in N

Answer 11

Γ ⊢ M : σ ___ Γ, x : σ ⊢ N : σ
Γ ⊢ let x = M in N : σ

Question 12

Regole di inferenza Fun_τ: fn x ⇒ M

Answer 12

_Γ, x : τ ⊢ M : τ _
Γ ⊢fn x ⇒ M : τ → τ

Question 13

Regole di inferenza Fun_τ: MN

Answer 13

Γ ⊢ M : τ→ τ ___Γ ⊢ N : τ
Γ ⊢ MN : τ