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.

Improve this question
$\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$
    – Andrej Bauer
    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

Reset to default

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.