Content deleted Content added
Add back inline citations per request |
m Avoid giving the idea that a topos is intensional for functions |
||
| (2 intermediate revisions by 2 users 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 57:
===First Kleene algebra===
The first Kleene algebra <math>\mathcal{K}_1</math> consists of the set <math>\mathbb{N}</math> with application <math>a b := \phi_a(b)</math>, where <math>\phi_a</math> denotes the <math>a</math>-th [[partial recursive function]] in a standard Gödel numbering.{{r|van-oosten|p=15}}{{r|bauer|p=29}}
This pca can also be [[relativization|relativized]] to an oracle <math>D \subseteq \mathbb{N}</math>: we define a pca <math>\mathcal{K}_1^D</math> with carrier <math>\mathbb{N}</math> by setting <math>a b := \phi^D_a(b)</math>, where <math>\phi^D_a</math> is the <math>a</math>-th partial recursive function with oracle <math>D</math>.{{r|van-oosten|p=15}}{{r|bauer|p=30}}
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>
| |||