Razlika između inačica stranice »Sustav F«
(Bot: Automatski unos stranica) |
m (bnz) |
||
| Redak 1: | Redak 1: | ||
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 [[polimorfizam (računarstvo)|polimorfizma]] u [[programski jezik|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. | 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. | ||
Trenutačna izmjena od 05:41, 25. ožujka 2022.
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.