search

rahulc29 / realizability

Experiments with Realizability in Univalent Type Theory
https://rahulc29.github.io/realizability/
Apache License 2.0
10 stars 1 forks source link

Treat partiality and construct Kleene's first algebra #7

Open rahulc29 opened 7 months ago

rahulc29 commented 7 months ago

An outline :

  1. Define the lifting monad $\mathcal{L}$
  2. Define the syntax primitive recursive functions
  3. Define $\mu$
  4. Interpret the syntax of partial recursive functions using the $\mathcal{L}$
  5. Use the syntax of partial recursive functions to create a (partial) combinatory algbera. No need for Godel codes.
  6. This should be equivalent to Kleene's first algebra.
rahulc29 commented 7 months ago

I'm not sure it would be possible to create a PCA using just the syntax. Godel codes are likely necessary.