与欧几里得几何的5条公理类似的10个LISP基元?

4
LISP可以由十个基本构件建立: 这些基本构件是:atom(原子),quote(引用),eq(相等性),car(首项),cdr(尾项),cons(组合),cond(条件语句),lambda(函数定义),label(循环语句),apply(函数应用)。
显然,它们相当于欧几里得几何的五条公理。 http://hyperpolyglot.wikidot.com/lisp 有人能解释一下它们是如何相等的吗?
6个回答

8
它只是说:
原语类比于欧几里得平面几何的五条公理。
这并没有表达等价性。据我所知,作者只是进行了类比,并想表达LISP是由其十个原子构建而成,就像欧几里得平面几何是由其五个公理构建而成一样。
虽然这个类比不太恰当。

3

您不需要那么多基本元素。仅使用LAMBDA就可以完成许多操作,例如整数数值等...

在现实生活中,Lisp具有更多基本元素。


1

艾伦·凯表达得很好:软件的麦克斯韦方程式

"...这是我读研究生时的重大启示,当我终于理解 Lisp 1.5 手册第13页底部的半页代码本身就是 Lisp 时。这些就是“软件的麦克斯韦方程式”!这几行代码代表了整个编程世界。"

摘自与艾伦·凯对话


1

真的吗?那么,我唯一能想到的就是所有欧几里得几何可以从这五个公理中推导出来(例如参见The Elements),就像显然所有LISP都可以从这十个基本操作构建出来。

对于好奇但懒惰的人,这里是欧几里得五个公理的一个表述,来自Wikipedia

  • 从任意一点向任意一点引一条直线。
  • 沿着一条直线无限延伸一条有限的直线。
  • 以任意圆心、任意距离作圆。
  • 所有直角相等。
  • 平行公设:如果一条直线在两条直线上落下,在同侧的内角小于两个直角,则这两条直线无限延伸会相交于内角较小的那侧。

1

它们是可比较的,因为它们足以实现所有Lisp,就像您可以从这些公理中推导出所有平面几何一样。但它们与几何特别无关。所以这不是等价性,只是一般相似性。

(欧几里得公设更有趣的一个属性是,您可以否定其中一个并获得一个不同的系统,该系统仍然非常有用(非平面几何)。但我不确定同样的情况是否适用于Lisp原语,我怀疑作者没有考虑到这一点。)


1

声明并不是说可以使用Lisp原语来证明平面几何中的定理。这样想是错失了类比的意义。我重新写了这句话,希望能够阻止人们这样思考。正确的类比并不新鲜;Graham的论文开头就指出,McCarthy“为编程做了类似于Euclid为几何学所做的事情。”

当设计Lisp时,McCarthy心中想着数学推理系统。在他1979年对Lisp历史的回顾中,他指出“现在更容易证明纯Lisp程序满足其规范,而对于任何其他广泛使用的编程语言来说都不容易。”这是因为Lisp原语具有引用透明性,这是它们与数学符号共享的特性。任何可以由这些原语实现的程序都具有这个特性。当你需要推理你的程序时,数学的整洁性会带来回报。

“证明即程序”的概念由Curry-Howard对应关系明确了。

参考资料:

McCarthy on "mathematical neatness"

Curry-Howard对应关系(维基百科)

Lisp的起源,Paul Graham

引用透明性(维基百科)


网页内容由stack overflow 提供, 点击上面的
可以查看英文原文,
原文链接