foundations.md

Definition

I guess I should define the terms first:

• small letters denote variable name, capital letters denote terms (exceptions below).
• $T$ denotes a type name.
• $\mathbf{V}$ denotes the set of all variable names.
• $\mathbf{F}$ denotes the set of all function names.
• $\mathbf{K}$ denotes the set of all constants.
• term definition:
  1. if $x\in \mathbf{V}\cup \mathbf{K}$ then $x$ is a term.
  2. if $f\in \mathbf{F}$, and $A$ and $B$ are terms, then so is $f(A,B)$.
• the functions have type signature $(T_1,T_2)\mapsto T_3$.
• $\mathbf{T}$ denotes any type i.e., type names as well as function types.
• $A:\mathbf{T}$ means that $A$ is of type $\mathbf{T}$.
• $\mathrm{\Gamma }$ denotes a set $X_0:=Y_0,X_1:=Y_1,\dots ,X_n:=Y_n$ of axioms (defined using the axiom keyword).
• $\mathrm{\Pi }$ denotes a set $X_1:{\mathbf{T}}_1,X_2:{\mathbf{T}}_2,\dots ,X_n:{\mathbf{T}}_n$ of type assignments (defined using the type keyword).
• in $A[x/Y]$, $x/Y$ denotes a pattern/replacement pair, where $x$ is a variable, while $Y$ is a term.
• the substitution algorithm $A[x/Y]$ is defined as follows:
  1. ${\displaystyle x[x/Y]=Y}$.
  2. ${\displaystyle a[x/Y]=a,a\in \mathbf{V}-\{x\}}$.
  3. ${\displaystyle k[x/Y]=k,k\in \mathbf{K}}$.
  4. ${\displaystyle f(A,B)[x/Y]=f(A[x/Y],B[x/Y])}$.

Foundations

The heart of nnoq is a single operator, :=, which is governed by the following axioms:
1. ${\displaystyle \frac{\mathrm{\Pi }⊢A:T}{\mathrm{\Gamma }⊢A:=A}}$ (reflexivity)
2. ${\displaystyle \frac{\mathrm{\Gamma }⊢A:=B\mathrm{\Gamma }⊢B:=C}{\mathrm{\Gamma }⊢A:=C}}$ (transitivity)
3. ${\displaystyle \frac{(A:=B)\in \mathrm{\Gamma }\mathrm{\Pi }⊢A:T\mathrm{\Pi }⊢B:T}{\mathrm{\Gamma }⊢A:=B}}$ (derivability from axioms)
4. ${\displaystyle \frac{\mathrm{\Gamma }⊢A:=B\mathrm{\Gamma }⊢C:=D\mathrm{\Pi }⊢f(A,C):T}{\mathrm{\Gamma }⊢f(A,C):=f(B,D)}}$ (congruence)
5. ${\displaystyle \frac{\mathrm{\Gamma }⊢A:=B\mathrm{\Pi }⊢A:T_A\mathrm{\Pi }⊢A[x/Y]:T_A}{\mathrm{\Gamma }⊢A[x/Y]:=B[x/Y]}}$ (substitution)

the following five axioms are for the type analysis (inference and checking):
6. ${\displaystyle \frac{}{\mathrm{\Pi },A:\mathbf{T},{\mathrm{\Pi }}^{\prime }⊢A:\mathbf{T}}}$ (derivability from type assignments/declarations)
7. ${\displaystyle \frac{(A:=b)\in \mathrm{\Gamma }\mathrm{\Pi }⊢A:T}{\mathrm{\Pi }⊢b:T}}$ (type inference from := #1)
8. ${\displaystyle \frac{(a:=B)\in \mathrm{\Gamma }\mathrm{\Pi }⊢B:T}{\mathrm{\Pi }⊢a:T}}$ (type inference from := #2)
9. ${\displaystyle \frac{\mathrm{\Pi },x:T_x⊢A:T_A\mathrm{\Pi },A[x/Y]:T_A⊢Y:T_x}{\mathrm{\Pi }⊢A[x/Y]:T_A}}$ (typed variable elimination)
10. ${\displaystyle \frac{\mathrm{\Pi }⊢f:(T_1,T_2)\mapsto T_3\mathrm{\Pi }⊢A:T_1\mathrm{\Pi }⊢B:T_2}{\mathrm{\Pi }⊢f(A,B):T_3}}$ (typed function instantiation)

nnoq builds on top of this foundation by generalizing the functions to arbitrary arity. however, this does not increase its power, as an n-arity function $f:(T_1,\dots ,T_n)\mapsto T_{ret}$ can be easily emulated in the core by n functions $f_1:(T_n,F_0)\mapsto F_1,f_2:(T_{n-1},F_1)\mapsto F_2,\dots ,f_n:(T_1,F_{n-1})\mapsto T_{ret}$ and a constant $f_0:F_0$.