Rachunek lambda z typami
Ten artykuł od 2016-11 wymaga zweryfikowania podanych informacji.
Należy podać wiarygodne źródła w formie przypisów bibliograficznych.
Część lub nawet wszystkie informacje w artykule mogą być nieprawdziwe. Jako pozbawione źródeł mogą zostać zakwestionowane i usunięte.
Sprawdź w źródłach: Encyklopedia PWN • Google Books • Google Scholar • Federacja Bibliotek Cyfrowych • BazHum • BazTech • RCIN • Internet Archive (texts / inlibrary)
Dokładniejsze informacje o tym, co należy poprawić, być może znajdują się w dyskusji tego artykułu.
Po wyeliminowaniu niedoskonałości należy usunąć szablon {{Dopracować}} z tego artykułu.
Część lub nawet wszystkie informacje w artykule mogą być nieprawdziwe. Jako pozbawione źródeł mogą zostać zakwestionowane i usunięte.
Sprawdź w źródłach: Encyklopedia PWN • Google Books • Google Scholar • Federacja Bibliotek Cyfrowych • BazHum • BazTech • RCIN • Internet Archive (texts / inlibrary)
Dokładniejsze informacje o tym, co należy poprawić, być może znajdują się w dyskusji tego artykułu.
Po wyeliminowaniu niedoskonałości należy usunąć szablon {{Dopracować}} z tego artykułu.
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
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.