Sustav F: razlika između inačica
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. | ||
Posljednja izmjena od 25. ožujak 2022. u 05:41
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
- Obrada nije uspjela. (MathML sa SVG ili PNG za rezervu (preporučljivo za moderne preglednike i alate za pristupačnost): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\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 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.