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.
[]
ornil
. 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. $\endgroup$