scientific article; zbMATH DE number 1463093
Several generalised type theories allow quantified types \(\forall X.\sigma\), where \(X\) is a type variable. If a term \(M\) has type \(\forall X.\sigma\) \((M:\forall X.\sigma)\), \(M\) can be interpreted as the proof of the quantified formula \(\forall X.\sigma\). If \(M:\forall X.\sigma\) it follows that for any type \(\rho\), \(M\rho:[\rho/X]\sigma\). The author wants to reverse this last procedure by finding an appropriate \(M:\forall X.\sigma\), given \(\sigma\) and \(N:[\rho/X]\sigma\). He defines, for a given type \(\sigma\), a type \(\rho\) to be generic and a term \(N\) to be a prototype proof of \([\rho/X] \sigma\) if there exists a term \(P\) such that \(P:\sigma\) and \([\rho/X] P=N: [\rho/X] \sigma\). (= is an extended \(\beta\eta\) equality and there are some restrictions on \(X\).) Given this generic type and prototype, \(\land X.P\), the abstraction of \(P\) w.r.t. the type variable \(X\), will be the required \(M\). He shows that given \(\sigma,\rho,X\) and \(N\), it is decidable whether \(\rho\) is generic and \(N\) is a prototype proof of \([\rho/X]\sigma\). He also shows that for a generic \(\rho\) and a prototype proof \(N\) of \([\rho/X]\sigma\), \[ [\rho/X] M=N= [\rho/X]M': [\rho/X] \sigma\Leftrightarrow M=M'. \]
- On Takeuti's early view of the concept of set
- Proving type class laws for Haskell
- What's so special about the Gödel sentence \(\mathcal{G}\)?
- Proceeding in Abstraction. From Concepts to Types and the Recent Perspective on Information
- scientific article; zbMATH DE number 1361532 (Why is no real title available?)
- A deflationary account of the truth of the Gödel sentence \(\mathcal{G}\)
This page was built for publication:
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4487253)
