Rachunek lambda z typami

Z Wikipedii, wolnej encyklopedii
Skocz do: nawigacja, szukaj

Rachunek lambda z typami to postać rachunku lambda rozszerzona o typy i z ograniczeniami, jakie wyrażenia są dozwolone, zależnie od ich typów.

Najprostszym takim rachunkiem jest rachunek lambda z typami prostymi.

Rachunek lambda z typami prostymi[edytuj | edytuj kod]

Typy są postaci: σ = κ | σ → σ, gdzie κ to zbiór typów bazowych

Ograniczenia to:

  • wszystkie wolne wystąpienia tej samej zmiennej mają ten sam typ
  • dla (Mσ1 Mσ2)σ3 : σ1 = σ2 → σ3
  • dla (λ x . Mσ1)σ2 : σ2 = σ3 → σ1 i wszystkie wystąpienia zmiennej x w M mają typ σ3

Ograniczenia te gwarantują, że każde wyrażenie można sprowadzić do postaci normalnej.