Sustav F

Sustav F, poznat i kao polimorfni lambda račun ili lambda račun drugog reda, je tipizirani lambda račun. Otkrili su ga neovisno logičar Jean-Yves Girard i računalni znanstvenik John C. Reynolds. Sustav F formalizira pojam parametarskog polimorfizma u programskim jezicima.

Baš kao što lambda račun posjeduje varijable nad funkcijama i vezanja nad njima, lambda račun posjeduje varijable nad tipovima i vezanja nad njima.

Na primjer, činjenica da identiteta ima tip oblika A→ A bi u sustavu F bila formalizirana kao sud

${\displaystyle \vdash \Lambda \alpha .\lambda x^{\alpha }.x:\forall \alpha .\alpha \to \alpha }$

gdje je α varijabla tipa.

Pod Curry-Howard izomorfizmom, sustav F odgovara logici drugog reda.

Sustav F, skupa s čak i ekspresivnijim lambda računaima, može biti shvaćen kao dio lambda kocke.

Nedovršeni članak Sustav F koji govori o računarstvu treba dopuniti. Dopunite ga prema pravilima Wikipedije.