Content deleted Content added
→First Kleene algebra: Add link Tags: Mobile edit Mobile web edit |
m Avoid giving the idea that a topos is intensional for functions |
||
| (One intermediate revision by one other user not shown) | |||
Line 1:
In [[theoretical computer science]] and [[mathematical logic]], specifically in [[realizability]], a '''partial combinatory algebra''' (pca) is an algebraic structure which abstracts a [[model of computation]]. The definition of pcas uses an idea from [[combinatory logic]]. The [[realizability topos]] over a pca is a model of higher-order [[intuitionistic logic]] where informally every function is
==Definition==
Line 77:
<references>
<ref name=van-oosten>{{ cite book | title = Realizability: an introduction to its categorical side | author = Jaap van Oosten | isbn = 9780444515841 | year = 2008 | publisher = Elsevier Science | pages = 328 }}</ref>
<ref name=bauer>{{ cite web | title = Notes on realizability | author = Andrej Bauer | website = [[GitHub]] | url = https://github.com/andrejbauer/notes-on-realizability/releases/download/release/notes-on-realizability.pdf | date = 2025-02-21 | access-date = 2025-02-21 }}</ref>
</references>
| |||