blob: d443be14d58c0ca0ae37d3c87c28679cdb145204 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
|
+++
title = "Realizability"
author = "Yann Herklotz"
tags = []
categories = []
backlinks = ["4e3"]
forwardlinks = ["4e5"]
zettelid = "4e4"
+++
Mathematitians like to work with abstract notions when proving theorems.
However, often we would like to compute with that same abstract notion,
so we want to find an equivalent model, or realizer, that will allow us
to do that. This realizer is special though, in that it is an element of
the set of partial combinator algebras (pca) ($r \in \mathbf{A}$).
One can then create an Assembly $S$, which is composed of a type $|S|$
and realizers which are part of $\mathbf{A}$. Then, it's necessary that
for each element in $|S|$ there is a realizer:
$r \Vdash p$ for $p \in |S|$ and $r \in \mathbf{A}$.
|
