Sustav F - Povijest promjena

WikiSysop: bnz

2022-03-25T05:41:31Z

bnz

←Starija inačica		Inačica od 05:41, 25. ožujka 2022.
Redak 1:		Redak 1:
	~~<!--'''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 [[polimorfizam (računarstvo)\|polimorfizma]] u [[programski jezik\|programskim jezicima]].		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.

WikiSysop: Bot: Automatski unos stranica

2021-08-23T03:03:49Z

Bot: Automatski unos stranica

Nova stranica

'''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.

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

:<math>\vdash \Lambda\alpha. \lambda x^\alpha.x: \forall\alpha.\alpha \to \alpha</math>

gdje je α [[varijabla|varijabla tipa]].

Pod [[Curry-Howard izomorfizam|Curry-Howard izomorfizmom]], sustav F odgovara [[logika drugog reda|logici drugog reda]].

Sustav F, skupa sa čak i ekspresivnijim lambda računaima, može biti shvaćen kao dio [[lambda kocka|lambda kocke]].

{{mrva-rač}}
[[Kategorija:Lambda račun]]