NuPRL 中的证明(Leftpad)

本次要用 CTT 来写 Leftpad¹，以说明即使不能实际运行 NuPRL 仍是个很好的 programming logic？(因为如下证明我是直接写的，没在 NuPRL 里跑)

Takes a padding character, a string, and a total length, returns the string padded to that length with that character. If length is less than the length of the string, does nothing.

问題到手，首先定义的是 string 的 axioms

$$\forall x: \mathbb{N}. Str(x) \in Type\\C \in Type\\ \forall x: \mathbb{N}, y: \mathbb{N}_x, a : Str(x). a\ !!\ y \in C\\ \forall x: \mathbb{N}, a : Str(x). length (a) =_{\mathbb{N}} x\\$$

这样就有了 index 和 length，以及如下的 concat

$\forall n,m: \mathbb{N}, a : Str(n), b : Str(m).\\a+b \in \{c:Str(n+m)| \forall x:\mathbb{N}_n. a\ !!\ x =_C c\ !!\ x \land \forall x:\mathbb{N}_m b\ !!\ x =_C c\ !!\ (n+x)\}$

以及为了方便，还要有个 repeat

$repeat \in \forall n : \mathbb{N}, a : Char. \{b:Str(n)|\forall x: \mathbb{N}_n.b\ !!\ x =_C a\}$

这样就可以开始证明 Leftpad 了，命題 formalize 如下

$\begin{align} \forall [n:\mathbb{N}].&\forall c:C, s: Str(n),l:\mathbb{N}.\\&{\tt if}\ l\leq n\\ &{\tt then}\ \{r:Str(n)| s = r\}\\& {\tt else}\ \{r:Str(l)|\forall x:\mathbb{N}_n. s\ !!\ x =_C r\ !!\ x\land\forall x: \mathbb{N}_{(l-n)} . r\ !!\ x =_C c\} \end{align}$

proof sketch，即算法实现，显然为

$\lambda c,s,l.{\tt if}\ l \leq_\mathbb{N} n\ {\tt then}\ s\ {\tt else}\ s+repeat(l-n,c)\ {\tt where}\ n = {\it length}(s) $

参考