[lisper]

> not based on the lambda calculus

> It matters because gensyms suck.

That makes no sense. The lambda calculus has nothing to do with symbols. Lisp introduced the concept of symbols, but Lisp and the Lambda Calculus are not the same thing.

> obviously I know nothing about Lisp

That is indeed becoming rather obvious.

[jcrites]

The Lambda Calculus does have to do with symbols and is defined in terms of them. Consider how application is defined. "λx.t" is an anonymous function that takes an input and substitutes it for the symbol "x" in the expression "t".

For example, given "λx.x+1" then "(λx.x+1)(z) => z+1". This reduction process is formally defined by the beta reduction rule, which says that "(λx.t)s" evaluates to "t[x:=s]".

"t[x:=s]" means "substitute the value s for the symbol x in expression t". E.g., x+1[x:=5] => 5+1

https://en.m.wikipedia.org/wiki/Lambda_calculus#Beta_reducti...

If by symbol you mean something different than variable, then I might agree, but the heart of lambda calculus is the rule set for lambda abstraction, application, beta reduction. Due to alpha equivalence you could say that lambda calculus is agnostic to symbols however. I suppose it depends on what you mean. (Lambda calculus is defined in terms of capture avoiding substitutions.)

[lisper]

> If by symbol you mean something different than variable, then I might agree,

Well, the real question is what Curtis means by symbol, as the answer he gave is rather cryptic. But since he specifically raised the issue of "gensyms", that seems to be a reference to a standard Lisp function that generates symbols, a first-class Lisp data structure, at run-time or, more usually, at macro-expansion time. Since Curtis has complained about macros in the past, I assumed this was what he was referring to. "Symbols" that exist only in the textual representation of the language and not as first-class data types are usually called "identifiers" rather than symbols precisely to avoid this sort of confusion.

In any case, it is an elementary exercise to define a formal computational system equivalent to the lambda calculus that uses integers rather than identifiers. Instead of λx.x you write λn where n is an integer. 0 refers to the value bound by the innermost scope, 1 to the value bound by the next outer scope, and so on. So, for example, λx.λy.x becomes λλ1. But of course, no one does this because it's completely pointless.