How do you represent LISP as mathematical / logical model?

I asked this in stackoverflow, but the question probably fits here better.

This question arose from the objection that LISP is regarded as a functional language with some simple principles, namely functions, variables, and operators that roughly correspond to predicates, propositional variables, and connectives in logic respectively.

How would you define recursive structure and "data is a function is a data" paradigm central in LISP as a mathematical model? How about list processing feature? Can we derive LISP from simple mathematical foundations starting from propositional logic up to some specific factored logic?

Surely there must be a model, not only for LISP, but many similar "old" languages. So, I'd like to know, what are the necessary concepts of mathematics to define LISP-like language.

Point is not on what paradigm LISP fits the best, but to find out the simplest mathematical model for the language in question.

Lately, I found this paper of McCarthy (1960) which may answer the question: http://www-formal.stanford.edu/jmc/recursive.pdf

Logic, arithemic and automata by Church (1962) also seems a useful source: http://www.mathunion.org/ICM/ICM1962.1/Main/icm1962.1.0023.0058.ocr.pdf

• You probably use the $\lambda$ calculus. – Yuval Filmus Aug 3 '17 at 6:39
• Read the definition of Scheme. Scheme is a small variant on Lisp and its language definition is pretty mathematical. – Gilles 'SO- stop being evil' Aug 3 '17 at 8:58
• More general question about the same topic was asked few years ago: cs.stackexchange.com/questions/9756/… – MarkokraM Aug 3 '17 at 9:23
• I was about to post John McCarthy's paper, but I found that you've probably already read it. I think it answers your question quite well. Lisp is more or less based on untyped $lambda$-calculus. Also, Sam's answer in cstheory.stackexchange.com/questions/24991/… is great. – xuq01 Aug 4 '17 at 4:24

"Old" programming languages like Fortran, Cobol and LISP arose before serious mathematical theory of programming languages was developed. They inspired the development of such theory, but are full of idiosyncracies and features which from a mathematical point of view can best be described as "warts". However, each of the old languages in essence has a mathematical core. We can extract their cores and see what mathematical models those have.

For LISP the core would be a small subset of Scheme. Let us focus just on the list processing part, and forget about the fact that in LISP and Scheme one can change state with setq and the like.

A small core for LISP could contain the atoms, S-expressions and functions, by which we mean some basic functions, $\lambda$-abstractions, and recursive functions. There are several ways to model this much of LISP, but perhaps the neatest is by domain theory.

Consider the following simplified statement about (a core of) LISP. Every value is

1. either an atom (a literal),
2. or a cons,
3. or a function.

Let us try to express this idea mathematically. We should find a set $D$ of LISP values which

1. contains the set $A$ of all atoms (whatever they are)
2. contains $D \times D$ because every cons is a pair of values (car and cdr)
3. contains $D \to D$ because "functions are data"

We can express this idea as a requirement that $$A + D \times D + (D \to D) \subseteq D.$$ Unfortunately, this is not possible because $D \to D$ is larger than $D$, unless $D$ contains just one element (but there are many atoms).

However, there is a way out: the set $D \to D$ of functions is larger than $D$ only if we take all functions -- but we only need to consider the computable functions, or some slightly larger set of them. Indeed, as was shown by Dana Scott a long time ago, we should look for a space $D$ (rather than a set) and then take $D \to D$ to be the space of continuous functions (because every computable map is continuous). As it turns out, there are several kinds of "spaces" that we could use, all of which have in common that they capture the idea of information content and information processing. I cannot go into technical details on how this is done, but you can read about domain theory to find out more.

Let us just think about what $D$ must contain. Of course, it contains various atoms, includnig an element corresponding to nil. Then, it contains all finite lists of elements, since a list (x1 ... xn) is just a lot of nested pairs (x1, (x2, ..., (xn, nil)). Next, it contains lot and lots of functions: anything that can be defined by a lambda, and with a bit of care also anything that can be defined by recursion.

In summary, the answer to your question is that the mathematical essence of LISP is a space $D$ which contains the atoms, its own product $D \times D$ and its own function space $D \to D$.

The stuff about logic and propositional connectives, you should forget that on the first round of studying mathematical models of LISP. Maybe come back to it later, and look up something like Curry-Howard correspondence and realizability.

• Excellent narrowing and broadening of the topic. I didn't realize the syntactic correspondence of the programs itself to the system of natural deduction. Very enlightening. – MarkokraM Aug 3 '17 at 18:05
• Historical and philosophical aspects of the question is well put by Philip Wadler in The Strange Loop conference 2015, "Propositions as Types" youtu.be/IOiZatlZtGU?t=25m14s . Cape revelation at the end shows some enthusiams over the topic. – MarkokraM Aug 5 '17 at 15:12