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

[math]\displaystyle{ \vdash \Lambda\alpha. \lambda x^\alpha.x: \forall\alpha.\alpha \to \alpha }[/math]

gdje je α varijabla tipa.

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

Sustav F, skupa sa č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 uređivanja Hrvatske internetske enciklopedije.