1
$\begingroup$

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.

$\endgroup$
9
  • $\begingroup$ What's your definition of computable function? There are no $LispTerm$ in Turing machine. $\endgroup$
    – Dmitry
    Aug 19, 2022 at 1:30
  • $\begingroup$ @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. $\endgroup$
    – prog
    Aug 19, 2022 at 12:45
  • 1
    $\begingroup$ 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. $\endgroup$
    – Dmitry
    Aug 19, 2022 at 20:41
  • $\begingroup$ 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). $\endgroup$ Aug 20, 2022 at 21:38
  • $\begingroup$ @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. $\endgroup$
    – prog
    Aug 22, 2022 at 13:32

0

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge that you have read and understand our privacy policy and code of conduct.