patternMinor
Dependent type system with different computation model
Viewed 0 times
computationwithsystemtypedifferentmodeldependent
Problem
There exist various Turing-equivalent models of computation, such as lambda calculus, Turing machines, or register machines.
It seems that dependent type systems (like Coq, Agda, Idris, homotopy type theory) all have a lambda-calculus-based model of computation at their core. That's because they use term substitution ($\beta$-reduction) to relate the typing model to the computation model.
Can we swap out the lambda calculus at the core of dependent type systems for other computation models?
Or more generally, can we formulate a type system that lets us plug in our own computation model and its inference rules, subject to some set of consistency rules?
It seems that dependent type systems (like Coq, Agda, Idris, homotopy type theory) all have a lambda-calculus-based model of computation at their core. That's because they use term substitution ($\beta$-reduction) to relate the typing model to the computation model.
Can we swap out the lambda calculus at the core of dependent type systems for other computation models?
Or more generally, can we formulate a type system that lets us plug in our own computation model and its inference rules, subject to some set of consistency rules?
Solution
Yes, realizability theory allows you to model dependent type theory based on a variety of computational models, such as: Turing machines (with or without oracles), various $\lambda$-calculi, topological models of computation, sequential functionals, game-semantics computational models, and many others.
References:
References:
- Jaap van Oosten: Realizability: an introduction to its categorical side, Studies in Logic and the Foundations of Mathematics, vol. 152, Elsevier, 2008
- You could also peek in Section 1.1. of my PhD thesis.
Context
StackExchange Computer Science Q#103831, answer score: 7
Revisions (0)
No revisions yet.