# Simple proof that Lisp expresses all computable list functions

Given computable function $$f : LispTerm \rightarrow LispTerm$$ is it possible to implement it in Lisp?

The $$LispTerm$$ is any term that is constructed using cons, nil and set-car!, set-cdr! (because it can be cyclic).

Of course Lisp is Turing-Complete, but that does not immediately imply an answer because Lisp would be Turing-Complete even if it didn't have cons without which we would not be able to construct a new $$LispTerm$$, and thus would not be able to implement all transformations. To be clear: Lisp interpreter reads not an "encoded version" of a $$LispTerm$$, such as a string representation of it, but literally the term itself, so that if there were no car operation in Lisp, then we would never be able to access first element of a $$LispTerm$$.

I am looking for a simple proof, or a reference, if it is a known fact. A proof that is probably too hard is one that requires to convert terms to natural numbers, then use the fact that on numbers Lisp is Turing-Complete, and then convert numbers back to terms. Unless there is an obvious way of converting cyclic terms to numbers and especially the other way.

## Computability in relation to $$LispTerm$$s

To say that function $$f$$ is computable means that there exists a structure preserving map $$h$$ between $$LispTerm$$s and binary strings (inputs of Turing Machines) such that if we use the mapping on $$f$$ resulting in a function $$g : \{0, 1\}^* \rightarrow \{0, 1\}^*$$, then $$g$$ is computable. The map $$h$$ is structure preserving iff $$\forall x, \forall y, f(x) = y \iff g(h(x)) = h(y)$$.

## Example $$LispTerm$$s

Objects like (cons nil nil) and (cons (cons nil nil) nil) are $$LispTerm$$s that can be constructed by the identical Lisp code. There are also cyclic terms. A cyclic term x = (cons x nil) could be constructed with the following Lisp code:

(define x (cons nil nil))
(set-car! x x)


Formally, $$LispTerm$$s are ordered graphs of degree 2, or functions of type $$f : V \rightarrow V^2$$, where $$V$$ is the set of nodes.

Function car returns first element of a $$LispTerm$$, and cdr returns the second element.

• What's your definition of computable function? There are no $LispTerm$ in Turing machine. Aug 19, 2022 at 1:30
• @Dmitry I added my understanding to the question, thanks for asking. My definition of computability is the same as in cs.stackexchange.com/questions/88610/… for example.
– prog
Aug 19, 2022 at 12:45
• If I understood the meaning of these Lisp functions correctly, this is not the definition you want. First, consider only the following subset of terms: lists whose elements are either [] or nil. For such lists, there exists a natural mapping to/from natural numbers, and hence you can naturally encode Turing machines using this set of terms. Lisp can't solve Halting problem, but it's possible according to your definition: you select the mapping $f$ so that $f(x)$ is odd if the Turing machine halts, and even if it doesn't halt. $g$ simply extract the last bit. Aug 19, 2022 at 20:41
• Why do you say that doing the proof via encoding with numbers is too hard? Also, you need to fix the definition of computable function, it's non-sensical (see Dimitry's remark). Aug 20, 2022 at 21:38
• @Dmitry, you are right, my bad. I fixed the definition of computability by adding the assumption that the mapping has to be structure preserving, which rules out the mapping that your proof uses.
– prog
Aug 22, 2022 at 13:32