11
$\begingroup$

I am studying the s-m-n theorem and the concept reminded me of currying.

From wikipedia article about s-m-n theorem:

the theorem says that for a given programming language and positive integers m and n, there exists a particular algorithm that accepts as input the source code of a program with m + n free variables, together with m values. This algorithm generates source code that effectively substitutes the values for the first m free variables, leaving the rest of the variables free.

From an article about currying:

Intuitively, currying says "if you fix some arguments, you get a function of the remaining arguments"

Seems like the same idea to me. The only reason why I am unsure is that the materials I came across on s-m-n don't mention currying (and vice versa), so I wanted to consult it to make sure I actually get it.

$\endgroup$
  • $\begingroup$ Indeed. Some computability proofs have a lambdish flavor. The s-m-n theorem, very roughly, allows to pretend that indexes of recursive functions are lambda terms, so that given $\phi_i(-,-)$ we can craft the informal $g(x) = \#\lambda y. \phi_i(x,y)$ and claim that $g$ is primitive recursive. Even the second recursion theorem proof (which exploits s-m-n) is Church's fixed point combinator in disguise, hidden behind $s()$ uses. The key point here is that even if the enumeration $\phi_i$ is defined enumerating, say, TMs (or Java, or ...) we can still pretend we have lambdas! $\endgroup$ – chi Sep 4 '17 at 14:00
  • $\begingroup$ Well, s-m-n makes an existential statement while the existence of a curried function provides the "compiler". But the idea is the same. $\endgroup$ – Raphael Sep 4 '17 at 14:05
14
$\begingroup$

Yes, it is the same thing.

Currying is a concept from $\lambda$-calculus. It is a transformation between $A \times B \to C$ and $A \to (B \to C)$. Think of this as "if we have a function of two arguments of types $A$ and $B$, then we may fix the first argument (of type $A$), and we will get a function of the remaining argument (of type $B$)". In fact, this transformation is an isomorphism. This is made mathematically precise by mathematical models of (typed) $\lambda$-calculus, which are cartesian closed categories.

There is a category of numbered sets. A numbered set is a pair $(A, \nu_A)$ where $A$ is a set and $\nu_A : \mathbb{N} \to A$ is a partial surjection, i.e., a map from numbers onto $A$, which may also be undefined. If $\nu_A(n) = x$ then we say that $n$ is a code of $x$. In computability theory there are many examples. Whenever we encode some information with a number we get a numbered set. For instance, there is a standard numbering $\varphi$ of partial computable functions, so that $\varphi_n(k)$ is the number computed by the partial computable function encoded by $n$ when applied to $k$. (The result may be undefined.)

A morphism of numbered sets is a realized map $f : (A, \nu_A) \to (B, \nu_B)$, which means that there exists $n \in \mathbb{N}$ such that $f(\nu_A(k)) = \nu_B(\varphi_n(k))$ for all $k$ in the domain of $\nu_A$. This looks complicated, but all it says is that $\varphi_n$ does to codes what $f$ does to elements. It is the mathematical way of saying that "program $\phi_n$ implements function $f$".

Here is the punchline: the category of numbered sets is cartesian closed. We may therefore interpret the typed $\lambda$-calulus in it, and ask what program implements the currying operation. The answer is: the program given by the s-m-n theorem.

$\endgroup$
  • $\begingroup$ Interesting. Is that category closely related to $PER(A)$? $\nu_A$ seems to induce a PER. $\endgroup$ – chi Sep 4 '17 at 14:06
  • 1
    $\begingroup$ Yes, the two categories are equivalent, and the third equivalent version is that of modest sets (lookup "modest sets and assemblies"). $\endgroup$ – Andrej Bauer Sep 4 '17 at 14:55

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.