There are three kinds of thing in the world: algorithms, problems, and machines. An algorithm may solve a problem, and a problem may be computed on a machine. If an algorithm \(x\) solves a problem \(X\), we write \(x\)\(:\,\)\(X\); if a problem \(X\) is computed on a machine \(\Gamma\), we write \(X\)\(:\,\)\(\Gamma\); when \(\xi\)\(:\,\)\(\Xi\), we say an object \(\xi\) is of type \(\Xi\) . In logic, an algorithm is called a proof, and a problem called a proposition, and a machine called a formal system. Sometimes when we call something a term, it can refer to any of them.
In type theory, we also introduce the concept of universes. A universe is a kind of super machine, so that a machine \(\Gamma\) can be thought as an instance of super machine \(\wp \vphantom{ \wp}_{n}\), which might not exist in reality; in that case, we write \(\Gamma\)\(:\,\)\(\wp \vphantom{ \wp}_{n}\).
A function maps objects from one type to objects another type. If a function \(\varphi\) takes an object \(\xi\)\(:\,\)\(\Xi\) as input and another object \(\vartheta\)\(:\,\)\(\Theta\) as output, we write \(\varphi\)\(\left[\vphantom{\xi :\, \Xi}\right.\)\(\xi\)\(:\,\)\(\Xi\)\(\left.\vphantom{\xi :\, \Xi}\right]\)\(\;\equiv\;\)\(\vartheta\)\(:\,\)\(\Theta\). The function is written as \(\underset{\xi :\, \Xi}{ \leftthreetimes}\)\(\vartheta\), of type written as \(\underset{x :\, X}{ \forall}\)\(\Xi\) .
We have countably infinite number of identifier symbols, which can denote any algorithms, problems, and machines—constant or variable—without any predetermined meaning. We also have countably infinite memory bits and countably infinite time slots. However, there are several fundamental rules we ought to obey.
In this series of notes I don’t intend to be rigorous, nor formal, but I stress the so-called Curry-Howard correspondence, whenever possible. I would abuse the notation for function, so that the function itself and its image is confused, as long as the image is not ambiguous. Thus if \(f\)\(\left[\vphantom{x}\right.\)\(x\)\(\left.\vphantom{x}\right]\)\(\;\equiv\;\)\(2\)\(x\), \(x\)\(\;\equiv\;\)\(3\)\(t\), then we write \(f\)\(\;\equiv\;\)\(2\)\(x\) and even \(f\)\(\left[\vphantom{t}\right.\)\(t\)\(\left.\vphantom{t}\right]\)\(\;\equiv\;\)\(6\)\(t\).
In the very beginning, we possess a primitive machine \(\wp \vphantom{ \wp}_{0}\), which can only compute decidable problems. At any rate, we at least have \(\wp \vphantom{ \wp}_{0}\) at our disposal. Therefore a machine is valid, if it is stronger than \(\wp \vphantom{ \wp}_{0}\). Especially, \(\wp \vphantom{ \wp}_{0}\) is valid. Put most plainly, if we have \(\wp \vphantom{ \wp}_{0}\), then we have \(\wp \vphantom{ \wp}_{0}\), namely:
Primitive:
\(\;\mathtt{has}\;\)\(\psi\)\(\left[\vphantom{\wp \vphantom{ \wp}_{0}}\right.\)\(\wp \vphantom{ \wp}_{0}\)\(\left.\vphantom{\wp \vphantom{ \wp}_{0}}\right]\)\(\;\equiv\;\)\(\wp \vphantom{ \wp}_{0}\)\(;\,\)
\(\;\mathtt{say}\;\)\(\Gamma\)\(\,\mathsf{is}\,\)\(\,\mathsf{valid}\,\)\(\,\mathsf{about}\,\)\(\wp \vphantom{ \wp}_{0}\)\(,\,\)\(\;\mathtt{if}\;\)\(\;\mathtt{has}\;\)\(\psi\)\(\left[\vphantom{\Gamma}\right.\)\(\Gamma\)\(\left.\vphantom{\Gamma}\right]\)\(\;\equiv\;\)\(\wp \vphantom{ \wp}_{0}\)\(;\,\)
Furthermore, \(\wp \vphantom{ \wp}_{0}\) realizes super machines \(\wp \vphantom{ \wp}_{1}\), and \(\wp \vphantom{ \wp}_{1}\) realizes super machines \(\wp \vphantom{ \wp}_{2}\), and so on:
\(\wp \vphantom{ \wp}_{0}\)\(:\,\)\(\wp \vphantom{ \wp}_{1}\)\(;\,\)\(\wp \vphantom{ \wp}_{1}\)\(:\,\)\(\wp \vphantom{ \wp}_{2}\)\(;\,\)\(.\)\(.\)\(.\)\(;\,\)
Clearly, with valid machines \(\Gamma\)\(,\,\)\(\Delta\), we get a valid new machine by combining \(\left\langle\vphantom{\Gamma ,\, \Delta}\right.\)\(\Gamma\)\(,\,\)\(\Delta\)\(\left.\vphantom{\Gamma ,\, \Delta}\right\rangle\). Actually, we may think \(\left\langle\vphantom{\Gamma ,\, \Delta}\right.\)\(\Gamma\)\(,\,\)\(\Delta\)\(\left.\vphantom{\Gamma ,\, \Delta}\right\rangle\)\(:\,\)\(\wp \vphantom{ \wp}_{1}\). With a valid composite of machines \(\Gamma\)\(,\,\)\(\Delta\), once \(\Gamma\) doesn’t depend on additional objects than \(\Delta\) does, we can use only \(\Delta\), namely:
Scope:
\(\;\mathtt{given}\;\)\(\left\langle\vphantom{\Gamma ,\, \Delta}\right.\)\(\Gamma\)\(,\,\)\(\Delta\)\(\left.\vphantom{\Gamma ,\, \Delta}\right\rangle\)\(\,\mathsf{valid}\,\)\(\,\mathsf{about}\,\)\(\wp \vphantom{ \wp}_{0}\)\(,\,\)\(\;\mathtt{has}\;\)\(\psi\)\(\left[\vphantom{\Gamma}\right.\)\(\Gamma\)\(\left.\vphantom{\Gamma}\right]\)\(\;\equiv\;\)\(\Delta\)\(;\,\)
Rule Scope corresponds to the deletion of superfluous variables in logic.
Suppose machine \(\Gamma\) can compute problem \(X\) . With \(\Gamma\), and with any algorithm \(x\) which solves \(X\), we have a valid new machine, namely:
Valid_problem:
\(\;\mathtt{given}\;\)\(\varphi\)\(\left[\vphantom{\Gamma}\right.\)\(\Gamma\)\(\left.\vphantom{\Gamma}\right]\)\(\;\equiv\;\)\(X\)\(:\,\)\(\wp \vphantom{ \wp}_{0}\)\(,\,\)\(\left\langle\vphantom{\Gamma ,\, x :\, X}\right.\)\(\Gamma\)\(,\,\)\(x\)\(:\,\)\(X\)\(\left.\vphantom{\Gamma ,\, x :\, X}\right\rangle\)\(\,\mathsf{is}\,\)\(\,\mathsf{valid}\,\)\(;\,\)
Suppose machine \(\Gamma\) can simulate \(X\) . With \(\Gamma\), and with any problem \(X\) which is computed on \(\Delta\), we have a valid new machine, namely:
Valid_machine:
\(\;\mathtt{given}\;\)\(\varphi\)\(\left[\vphantom{\Gamma}\right.\)\(\Gamma\)\(\left.\vphantom{\Gamma}\right]\)\(\;\equiv\;\)\(\Delta\)\(,\,\)\(\left\langle\vphantom{\Gamma ,\, X :\, \Delta}\right.\)\(\Gamma\)\(,\,\)\(X\)\(:\,\)\(\Delta\)\(\left.\vphantom{\Gamma ,\, X :\, \Delta}\right\rangle\)\(\,\mathsf{is}\,\)\(\,\mathsf{valid}\,\)\(;\,\)
Or, including super machines:
\(\;\mathtt{given}\;\)\(\varphi\)\(\left[\vphantom{\Gamma :\, \wp \vphantom{ \wp}_{n \,+\, 1}}\right.\)\(\Gamma\)\(:\,\)\(\wp \vphantom{ \wp}_{n \,+\, 1}\)\(\left.\vphantom{\Gamma :\, \wp \vphantom{ \wp}_{n \,+\, 1}}\right]\)\(\;\equiv\;\)\(\wp \vphantom{ \wp}_{n}\)\(,\,\)\(\left\langle\vphantom{\Gamma ,\, \Delta :\, \wp \vphantom{ \wp}_{n \,+\, 1}}\right.\)\(\Gamma\)\(,\,\)\(\Delta\)\(:\,\)\(\wp \vphantom{ \wp}_{n \,+\, 1}\)\(\left.\vphantom{\Gamma ,\, \Delta :\, \wp \vphantom{ \wp}_{n \,+\, 1}}\right\rangle\)\(\,\mathsf{is}\,\)\(\,\mathsf{valid}\,\)\(;\,\)
Rules ValidProblem and ValidMachine correspond to universal instantiation in logic.
Suppose we have such a method, that, with machine \(\Gamma\), and with any \(x\) an implementation of \(X\), we can solve problem \(Y\) . Then, with \(\Gamma\), we may obtain a solution which takes any \(x\) and solves \(Y\), namely:
Elimination_problem:
\(\;\mathtt{given}\;\)\(\varphi\)\(\left[\vphantom{\Gamma ,\, x :\, X}\right.\)\(\Gamma\)\(,\,\)\(x\)\(:\,\)\(X\)\(\left.\vphantom{\Gamma ,\, x :\, X}\right]\)\(\;\equiv\;\)\(Y\)\(:\,\)\(\wp \vphantom{ \wp}_{0}\)\(,\,\)\(\;\mathtt{has}\;\)\(\psi\)\(\left[\vphantom{\Gamma}\right.\)\(\Gamma\)\(\left.\vphantom{\Gamma}\right]\)\(\;\equiv\;\)\(\underset{\bar{x} :\, X}{ \forall}\)\(Y\)\(\left[\vphantom{\bar{x}}\right.\)\(\bar{x}\)\(\left.\vphantom{\bar{x}}\right]\)\(:\,\)\(\wp \vphantom{ \wp}_{0}\)\(;\,\)
Suppose we have such a method, that, with machine \(\Gamma\), and with any \(x\) an implementation of \(X\), we can simulate machine \(\Delta\) . Then, with \(\Gamma\), we may obtain a machine which takes any \(x\) and simulates \(\Delta\) , namely:
Elimination_machine:
\(\;\mathtt{given}\;\)\(\varphi\)\(\left[\vphantom{\Gamma ,\, x :\, X}\right.\)\(\Gamma\)\(,\,\)\(x\)\(:\,\)\(X\)\(\left.\vphantom{\Gamma ,\, x :\, X}\right]\)\(\;\equiv\;\)\(\Delta\)\(,\,\)\(\;\mathtt{has}\;\)\(\psi\)\(\left[\vphantom{\Gamma}\right.\)\(\Gamma\)\(\left.\vphantom{\Gamma}\right]\)\(\;\equiv\;\)\(\left\langle\vphantom{x :\, X ,\, \Delta}\right.\)\(x\)\(:\,\)\(X\)\(,\,\)\(\Delta\)\(\left.\vphantom{x :\, X ,\, \Delta}\right\rangle\)\(;\,\)
Or, including super machines:
\(\;\mathtt{given}\;\)\(\varphi\)\(\left[\vphantom{\Gamma :\, \wp \vphantom{ \wp}_{n} ,\, x :\, X}\right.\)\(\Gamma\)\(:\,\)\(\wp \vphantom{ \wp}_{n}\)\(,\,\)\(x\)\(:\,\)\(X\)\(\left.\vphantom{\Gamma :\, \wp \vphantom{ \wp}_{n} ,\, x :\, X}\right]\)\(\;\equiv\;\)\(\Delta\)\(:\,\)\(\wp \vphantom{ \wp}_{n}\)\(,\,\)\(\;\mathtt{has}\;\)\(\psi\)\(\left[\vphantom{\Gamma}\right.\)\(\Gamma\)\(\left.\vphantom{\Gamma}\right]\)\(\;\equiv\;\)\(\underset{\bar{x} :\, X}{ \forall}\)\(\Delta\)\(\left[\vphantom{\bar{x}}\right.\)\(\bar{x}\)\(\left.\vphantom{\bar{x}}\right]\)\(:\,\)\(\wp \vphantom{ \wp}_{n}\)\(;\,\)
Rules ElMachine and ElProblem correspond to the deduction theorem in logic.
Suppose on machine \(\Gamma\), any algorithm \(x\)\(:\,\)\(X\) gives rise to an object \(\xi\)\(:\,\)\(\Xi\) . Then on machine \(\Gamma\), this map can properly define a function, namely:
Abstraction:
\(\;\mathtt{given}\;\)\(\varphi\)\(\left[\vphantom{\Gamma ,\, x :\, X}\right.\)\(\Gamma\)\(,\,\)\(x\)\(:\,\)\(X\)\(\left.\vphantom{\Gamma ,\, x :\, X}\right]\)\(\;\equiv\;\)\(\xi\)\(\left[\vphantom{x}\right.\)\(x\)\(\left.\vphantom{x}\right]\)\(:\,\)\(\Xi\)\(\left[\vphantom{x}\right.\)\(x\)\(\left.\vphantom{x}\right]\)\(,\,\)\(\;\mathtt{has}\;\)\(\psi\)\(\left[\vphantom{\Gamma}\right.\)\(\Gamma\)\(\left.\vphantom{\Gamma}\right]\)\(\;\equiv\;\)\(\underset{\bar{x} :\, X}{ \leftthreetimes}\)\(\xi\)\(\left[\vphantom{\bar{x}}\right.\)\(\bar{x}\)\(\left.\vphantom{\bar{x}}\right]\)\(:\,\)\(\underset{\bar{x} :\, X}{ \forall}\)\(\Xi\)\(\left[\vphantom{\bar{x}}\right.\)\(\bar{x}\)\(\left.\vphantom{\bar{x}}\right]\)\(;\,\)
Suppose on machine \(\Gamma\), there is a function of type \(\underset{\bar{x} :\, X}{ \forall}\)\(\Xi\)\(\left[\vphantom{\bar{x}}\right.\)\(\bar{x}\)\(\left.\vphantom{\bar{x}}\right]\) . Then on machine \(\Gamma\), this function can map any algorithm \(y\)\(:\,\)\(X\) to an object \(\xi\)\(\left[\vphantom{y}\right.\)\(y\)\(\left.\vphantom{y}\right]\), by replacing all occurrences of \(x\) with \(y\) , namely:
Application:
\(\;\mathtt{given}\;\)\(\varphi\)\(\left[\vphantom{\Gamma}\right.\)\(\Gamma\)\(\left.\vphantom{\Gamma}\right]\)\(\;\equiv\;\)\(\xi\)\(:\,\)\(\underset{\bar{x} :\, X}{ \forall}\)\(\Xi\)\(\left[\vphantom{\bar{x}}\right.\)\(\bar{x}\)\(\left.\vphantom{\bar{x}}\right]\)\(\;\mathtt{and}\;\)\(y\)\(:\,\)\(X\)\(,\,\)\(\varphi\)\(\left[\vphantom{\Gamma ,\, y}\right.\)\(\Gamma\)\(,\,\)\(y\)\(\left.\vphantom{\Gamma ,\, y}\right]\)\(\;\equiv\;\)\(\xi\)\(\left[\vphantom{y}\right.\)\(y\)\(\left.\vphantom{y}\right]\)\(:\,\)\(\Xi\)\(\left[\vphantom{x \:\leftarrow\: y}\right.\)\(x\)\(\:\leftarrow\:\)\(y\)\(\left.\vphantom{x \:\leftarrow\: y}\right]\)\(;\,\)
Rules Abstraction and Application correspond to conditional proofs and modus ponens in logic.
❧ May 21, 2021; extended August 9, 2021
References
❉ T Coquand and G Huet, ‹The Calculus of Constructions›. «Information and Computation», 1988
❉ V Voevodsky et al, «Homotopy Type Theory»