Toggle menu
309,6 tis.
57
18
527,9 tis.
Hrvatska internetska enciklopedija
Toggle preferences menu
Toggle personal menu
Niste prijavljeni
Your IP address will be publicly visible if you make any edits.

Sustav F

Izvor: Hrvatska internetska enciklopedija

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

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.