Izomorfizm Curry'ego-Howarda

Z Wikipedii, wolnej encyklopedii
Skocz do: nawigacja, szukaj

Izomorfizm Curry'ego-Howarda - określenie odpowiedniości pomiędzy termami rachunku lambda z typami a dowodami logiki intuicjonistycznej. Odpowiedniość ta pozwala na wyrażanie dowodów twierdzeń jako funkcji, co stało się podstawą dla licznych systemów dowodzenia twierdzeń opartych na logice intuicjonistycznej, takich, jak np. Coq[1].

Przypisy

Linki zewnętrzne[edytuj | edytuj kod]

  • Lambda Calculi With Types - artykuł Henka Barendregta omawiający rachunki lambda z typami i odpowiadające im systemy logiczne.