给货币加上类型 : RCast 35 译文

  • A+
所属分类:RChain新闻

《RCast 35 一个非典型性货币》译文 
 译者 RChain中文社区:莫给机狂
原文网址:  https://blog.rchain.coop/blog/2019/07/18/rcast-35-atypical-currency/

译者摘要:RCast是RChain合作社的一个播客,每周一次。一般是Greg和其他技术人员的访谈,主题一般是对RChain的技术的解释和深入探讨。从RCast可以学习到很多区块链的前沿的内容,可扩展性、安全性等等。从这个系列也可以看出Greg对区块链技术研究的深入程度。

根据译者的总结,这次讲座的几个重要结论:

  1. 货币可以有类型吗? 结论是可以。无类型的货币类似void*指针,有类型的货币是类型转换后的指针,或者是加了使用限制的货币。这种“带了类型”的货币,或者说加了使用限制的货币,未来可以有很多有趣的玩法,带来很多可能
  2. 并发系统用图灵机模型来分析、验证是很不合适的,不可避免会陷入状态空间的指数爆炸。Rho演算则可以
  3. 基于图灵机的合约之间没法度量相似性。但Rho演算可以,所以可以建立起基于合约行为额搜索系统
  4. 以太坊的合约,或者所有基于图灵机模型的合约,你都没法判断、约束合约的行为。Rho演算可以

=======================================================

以下是正文

Greg:今天我想谈谈一个非常奇怪的想法。它会让许多人感到奇怪。希望我可以激发这个思路,然后进入更高技术深度的探讨。我们的想法是从编程概念的角度来思考货币(资本,货币)。从计算角度来看,货币是无类型的 ;而这是个属性恰恰是它采用的最大理由。如果你回到资本的起源,这个无类型的特性就是为什么它首先被采用的原因:你可以将钱转换成任何东西,任何东西都可以转化为金钱。就这样子。

大家在市场上用贝壳进行交易,然后送货物上门—— 几捆干草、若干桶鱼、几桶啤酒等等,这样子做要比送这些货物运到市场再进行交换更高效。如果没卖掉,你还得将一大堆的东西拉回来,其中一些会坏掉。通过符号形式进行价值交换,将这个交换映射回商品和服务的交付,效率会高的多。

这种高效率已扩展到基于电子和互联网的市场,深刻的影响着我们的生活。但因为任何听这个播客的人都是在货币产生之后诞生的,所以他们很难想象货币产生之前的非常不便的交易场景。

如果我们从计算或计算的角度来看这个问题,事情会变得更加清晰。这种将任何货物转化为金钱再将金钱转化成货物的能力,对应的其实就是对某种东西设定价格。有一句古老的格言:每样货物、每个人都有自己的价格。这个格言其实就是指我们可以为某个东西设定价格。正因为我们可以为某种东西设定价格,我们可以奇迹般地将水变成葡萄酒:我们有水的价格,同时也有有葡萄酒的价格。这是这个属性的本质。

如果我们是C或C ++程序员,那么这个特性在类型级别是void *。如果我有一个指向任何类型的数据类型的指针,我总是可以将它转换为void *,然后我得到一个指针,它指向一样东西,但是没有任何类型信息。在像C和C ++这样的语言中,这就是所谓的向上类型转换。我丢掉了类型信息,这意味着我要走向类型层次结构的顶端,这意味着我的信息越来越少。相反,当我在类型层次结构中向下走时,我获得了信息。

如果我对一个void *指针进行类型转换然后进行一些操作,例如:序列化数据并将其通过一个信道传输到另一个地方然后反序列化。现在我想弄清楚指针指向的是什么类型的东西。向下类型转换就是声称这个void *指针指向一个特定的东西,比如一个指向整数的指针,或者指向一个结构的指针。

这种向下转换是不安全的:由于我们丢失了所有类型信息,我们不知道指针指向的是否真的是我们判断的那种东西,除非进行一些额外的检查。在像Javascript这样的语言中,这相当于说我得到的是一个对象。这样做我们就到了类型结构树的最顶端。在Java中,就是说,我有一个对象,但我忘记了所有类型信息。一旦我丢失了,或者忘记了这些信息,想要恢复过来,那这些信息就必须在这个信道之外额外提供。这就是个问题,事情可能会因为这样出岔子。额外提供信息就是说,我需要另外一个辅助信道来传输信息类型。

信息量很大吧,这听起来有道理吗?

Isaac: 是的,当然。我真的很喜欢这个钱/货币与类型转换/类型信息的类比。从本质上讲,这对应于你可以使用什么货币去换取任何东西。这是一个非常棒的思路。

Greg: 很高兴引起了你的共鸣。这是这些最大优点和最大弱点的取舍之一。货币的最大优点在于它允许我们转换为任何可以设置价格的东西,但是牺牲的是没有客观的估值体系。没有一个我们一致认可的标准,使我们能够对事物的估值进行客观评估。

我们经常可以看到这种情况的发生。由于这种货币的特性,董事会可以通过一种方式评估CEO,而股东则以不同的方式评价CEO。没有客观的评价准则,所以只能让法庭来决定。法庭的裁决也是基于某种社会评判准则,但这种准则也不具备客观性。

如果您按照这个类比进入编程世界,我们就会知道问题所在:缺乏类型安全性。无论你何时缺乏类型安全性,你都会遇到这中 “这个对象不是你认为的那样”的错误。你以为是水,但实际上是葡萄酒。

Isaac:我觉得这个没多大问题啊。

Greg: 哈,如果你是开发者,那就不爽了。这是C++或Javascript程序中许多运行期错误的根源,因为在这些语言中你没有类型安全。即使在强类型语言Haskell中,也有一些方式可以绕过类型安全性,这样结果就会变得悲惨。这种用牺牲类型安全来换取便捷性是很不明智的。

所以问题是:我们可以为货币添加类型安全吗?我们可以创造一个带类型的货币的概念吗?在区块链世界中,它是一个尚待探索的领域。我们正在研究各种不同的金融工具,因为区块链带来了很多可能性。现在我们可以对用软件实现一个货币,人们开始意识到货币不是上帝赐予的东西,而是人类的一项发明。我们可以探索它在未来的可以用来扮演什么角色。

我们是否有另外的方式来配置、组织货币体系,以便它可以更好地完成现有的任务,或者可以发掘出它新的使用方式?这是区块链能做的最奇妙的事情之一。2015年,我与Vlad(译者注:以太坊Casper协议之父,RChain董事会成员)以及另一个区块链研究者坐在一起进行视频访谈。他们在讨论如何设计金融工具来达到某些效果。令我震惊的是,通过区块链,即使是小孩也可以用设计游戏同样的方式来设计金融工具。把人类活动游戏化是小孩的第二天性,就像对我们大多数人来说,能够管理银行账户也是第二天性(好吧,至少对我们中的一些人来说是) 。

这种貌似高阶的能力——能够设计货币和金融工具,以便让一些活动游戏化,只是人们第二天性而已。他们一生都在这样做。今天的从来没有在互联网发明之前生活过的孩子们,不用教就能学会用手机使用谷歌、谷歌地图或其他数百种服务,这就是一种第二天性,与生俱来的。这是一个非常好的机会,可以设计一些现在的货币所缺失的东西,特别是,一个“有类型”的货币会是什么样子? “无类型”的货币和 “有类型”货币之间的最大区别在于是否能够约束或限制货币可以交换的对象。

Isaac:这完全有道理。

Greg: 有些市场就是这样有交换对象的限制的。比如外汇交易是成对的:“我可以用美元换成日元,或者用欧元换成里拉”。 这些兑换对里面,交易对象天然就是受限的。所以“加上限制的货币”不是一个凭空想象的东西。

我们知道即使在当今的金融市场中,某些金融工具也是带有限制的:你只能把钱转化为特定的东西。现在我们希望把这个概念通用化,用在日常生活中。这不是一个凭空想象的东西。

我们可以鱼与熊掌兼得吗?是否存在某种极简的模型,我们可以从本质出发构建出一个货币,同时这个货币只有一种东西可以兑换?

我们来设想一个交易场景,当我们处于交易中时,只有一样东西可以用于交换。我们去市场,如果没有这个东西(无论是贝壳还是比特币),我们就无法进行交易。

有趣的是,这正契合Rho演算的观点。Rho演算中,如果我们要做一个交易,这是一个Comm事件(译者注:Rho演算的基本演算规则),那么只有一样东西可以交换,那就是代码。Pi演算也是如此:只有一样东西可以交换,这就是名字。但Pi演算做不到的是将名字和进程关联起来。

但事实上,你可以建立这种名字和进程的关联的。Davide Sangiorgi提出一个“高阶Pi演算”的演算法,使得你也可以把过程进行传输。然后他证明这个高阶Pi演算可以完整的转化为普通的Pi演算。的确,你可以通过这种方式建立名字与行为的关联,但在Rho演算中,这种关联这是直接的,不用通过这种方式间接转换。

正是这种直接的关联让我们可以约束交易的对象。我在1999年从Pi演算的角度来看了货币的这个特点。到2002年,我看到了Rho微积分,就把这些概念串起来了。在1999年,我看着这个,我想,“噢,天哪,如果我在公开场合谈论这个思路,经济学家们会喷我“你对经济学、交易行为这些一无所知”。计算机科学家也会喷我:“你到底想做什么?”

然后我想最好还是保持沉默,即使我认为这是一个非常重要的想法。它使我们对货币产生了很多疑问。从某种意义上说,Rho演算是为了这个想法而产生的,这就是我提供这些历史背景的原因。

下一个重要的节点是LADL和名字空间逻辑。大约在2002 - 2003年,Caires和Cardelli开始关注空间逻辑。他们认为空间逻辑使人们能够了解程序的结构。例如可以有公式用来来检查一个进程是否由两个并行进程组成。

有一个著名的定理,它是关于互模拟与Hennessy-Milne逻辑之间关系的最重要的定理之一:空间行为逻辑是Hennessy-Milner逻辑的精细化。对于那些不了解背景的人来说,Henness-Milner逻辑是一种模态逻辑:除了“True”与“False”,否定、推断、以及不动点运算之外,您还可以研究一段程序的演化(运行)。

(译者注:互模拟(bisimulation)是个理论计算机机科学中的概念,指两个状态转换系统之间的二元关系,表明这两个系统行为类似。参见:https://en.wikipedia.org/wiki/Bisimulation )

在Pi演算或Rho演算的情况下,一段程序的演化仅通过comm事件发生。你可以推断某个特定输入/输出组合是否可能,或者是否一定会发生。一个comm事件要么通过输出,要么通过输入,只能通过其中一条路径离开当前状态。无论这个进程是什么,它都必须做通过这个IO事件才能演化(运行)。

这就是Hennessy Milner逻辑。这个逻辑有一个特性:两个进程P和Q互模拟(即进程代数中的“等价”),当且仅当对于任意公式T,进程P满足T和进程Q符合T同时发生. (译者注,原文公式用P来代表,和进程P重合带来了歧义,这里换成别的符号)

这是一个漂亮的定理,Hennessy-Milner逻辑清晰地表达了互模拟。

Isaac:嗯,公式将非互相似的过程区别开了

Greg: 完全正确!现在你可以做各种疯狂,怪异,有趣的事情。一个例子: 假设我们对所有的Hennessy-Milner公式们进行了定义良好的排序。接下来你可以用它来构建出两个进程之间的距离:顺序遍历这个有序的公式列表,直到到达第一个两个进程不满足的公式为止。那个距离,这个无限列表中,这两个进程满足的前部子序列长度,度量了它们相隔多远。你可以用这些信息做各种有趣,疯狂的事情。这可能是另一个RCast的主题。

(译者注:星云链吹嘘的合约的搜索,其实基于图灵机模型的合约是做不到,因为你没法把虚拟机代码当作字符串一样来搜索。字符串之间有定义良好的距离函数,可以所以可以进行搜索和匹配,但是这一点代码做不到。但是RChain中这个能力是能做到的。上面说的这个距离度量了两个合约的相似性)

空间逻辑增加了结构信息。对于Pi演算或Rho演算的这种交错执行的语义,互模拟并不区分并发执行和交错执行。这意味着每个并行运行的代码组合都可以转换成一个巨大的总和项,对应所有可能的IO交错执行的序列。(译者注:比如a,b,c,d 4个进程,交错执行下会有很多可能的序列,比如a->b->c->d,a->c->b->d, d->a->c->b等等,但是都可以用a|b|c|d来表达)使用Hennessy-Milner逻辑,您无法通判断进程内部是这样一个的总和项,还是并发执行的“|”项。

关于这个并发执行的“|”的重要之处正是这种表现力——你用一个“|”符号替换了所有可能交错执行序列的总和,不然就会指数爆炸。所以P|Q代表了所有P和Q交错执行的可能途径的合集。过程演算的表现力的很大一部分,就是克服了这种指数爆炸,这就是为什么它们比状态机计算模型要优越。 (译者注:状态机就是现有的绝大多数区块链项目的图灵机计算模型,每条虚拟机指令表达了虚拟机状态的转换规则)

我从这来之不易的经历中意识到:如果你试图在并发系统中用状态机来建模,那么这种交错执行会导致指数爆炸,最终让模拟器瘫痪。然而,如果有了并发的“|”符号后,你却可以在代数层面操作。只要你保持在代数层面操作,你就不必展开所有可能的交错执行序列。你可以以轻而易举的做到这一点。结果就是,用这个思路,您可以在计算方面做的更多的牛逼的东西。在很多方面,Rholang的力量的本源正是处于这个。很多牛逼的东西隐藏在我们正在做的项目中,我们还没有时间来谈论。(译者注:并发状态下合约的形式化验证,基于图灵机的都很难做,正因为这个状态指数爆炸问题。但是RChain没这个问题。)

我会在很快把这个发现回到“带类型的”货币这个主题上。但再此之前,我必须提供一些背景信息。空间逻辑类似X透视仪: 他们可以看到你的进程里有一个“|”符号,这会使得上述的互模拟特征定理失效。但是如果你添加一个和“|”符号的等价关系对应的观察结果集, 那么所有IO事件实际上都是所有可能的观察结果集,它本质上是一个可交换的幺半群或者类似的概念。这样可以继续使得这个定理成立。

能够看到你做了一个结合律操作,交换律的操作,所有这些都能重现你需要的观察结果,以便重新建立起公式和互模拟之间的对应关系。这种对应关系保持下来了。这非常重要,因为到目前为止,所有过程等价性都是通过互模拟来实现的。 (译者注:这两段太理论,可以不管。本质上是说即使加了并发的“|”符号,互模拟特征定理照样成立)

Isaac: 你有关于你提到的结果的链接吗?

Greg: 是的。我们可以把它放在链接中。这意味着如果你研究互模拟,那就是你需要学习的全部内容。对于像我这样拥有一个小脑袋的人来说,知道我可以抛开并发计算等价性的一堆概念,只需关注这一点,而其他的都是这一点的特例,这是一个巨大的进步。我可以让我的大脑清楚些。

因为现在我们有了对一个过程结构进行X射线透视的能力。在这里,我隐含的地引用了Curry-Howard。每当我说公式(Formulae)时,我也会说类型。如果我设计出一个对象为行为的公式系统,那么在Caires的体系(译者注:这里指高阶Pi演算)里,对于传输的名字的结构并没有太多阐述,因为它们是互不先关的。在Pi演算中,名字与过程的行为之间没有关系。但Rho演算完全不同。

Isaac:(Rho演算中名字和过程)有非常紧密的关联

Greg: 没错。现在让我们谈谈我们可以做的一些有趣的事情。一旦我有了一个对行为的类型系统,我就已经有了一个对名字的类型系统。现在让我们假设我不允许解引用发生(译者注:解引用即deference,在Rho演算中就是把名字转换为进程或者程序的操作)。我可以用构造性,或者否定性两种办法作为限制解引用 的方式。我们可以使用类型系统来限制解引用(即将名称重新转换为进程)发生,因为解引用是唯一可以创建新名字的方法。

这在Rho演算中是显而易见的。本质上,解引用在功能上和与反引号在Lisp中相同,或者和带前缀的逗号在基于Lisp的宏系统中执行相同。拼接到一个括号内的表达式,是一些可以被计算的表达式。这是允许你构造新名称的唯一机制。

这意味着,如果我想拥有一个固定总量的名字的供应,换句话说,固定的货币供应量, 通过设置这个限制:不允许解引用,那么就相当于你永远不能传递给我一个“铸币”的行为,我不允许将“铸币”实例化。

前面我们在几个理论中绕了这么多,但就我们面前的系统——Rho演算而言,只是如此一个简单的想法,我们已经能够实现控制货币的供应。

我们也可以要求货币总量应该不断减少,或者要求货币总量应该存在平衡。如果我们开始将货币的类型作为名字空间,比如说我们有来自红色名字空间的名字和来自蓝色名字空间的名字,我们还可以要求,如果你从红色命名空间发起交易,那么你就必须要在蓝色的名字空间结束交易。

你可以根据货币的使用场景创建各种平衡的Perrin风格的行为(译者注:这里不知道Perrin指的是哪一个,可能是研究区块链/数字货币法律和合约的专家Courtney Rogers Perrin ),这可以让你在类型级别来创建类似外汇交易的金融工具。最终的结果是,在一个社区里你完成了货币的分配:你从一个特定的货币分配开始,如果如果您铸造新的货币,最终会得到另一个不同的指定的货币分配。

这就像配平化学方程式一样。你永远不会创建任何元素。你总是只是改变元素的打包方式。在盐的例子中,你不是在制造钠元素或者**元素,它们只是在一起被包装成氯化钠,然后你就得到了盐。

所有这类涉及到货币的打包和分配的行为,都可以用命名空间清晰的表达。这绝对值得深入研究。现在RChain已经接近主网,我现在提出这一点的一部分动机是接触青少年社区并跟他们说:“嘿,这里有一大堆没人想到过的玩具。” 如果考虑将货币作为我们的社会协调技术之一,那RChain将为大家提供一个从所未见的将行为来游戏化的工具集。

我正在阅读Yuval Noah Harari的一系列书籍。他一次又一次地指出,智人与其他物种的区别在于我们的超级能力来自于他们之间的协调。我觉得我们必须强化这种协调能力来应对气候变化。令人惊讶的幸运是,就在我们需要升级这个协调能力的时候,这个牛逼的协调工具箱子恰好被我们打开了。这真是很奇怪。

Isaac: 有点宿命论的味道

Greg: 通常情况下,你总是可以在需要时找到所需的东西。需求是发明之母。你的头脑会变得专注:“天啊,我现在真的需要这个东西。”我觉得这(RChain)就是一个功能非常丰富的协调工具箱。

另一点是艺术是漫长的,生命是短暂的。我已经能够实现这一想法。我敢肯定,如果继续研究这个东西,我会不断提出越来越多的有趣的金融工具和用例。

Vlad和那个区块链研究员正在做的事情让我受到了很大启发,他们已经非常深入的了解了如何使用金融工具将人类行为游戏化。我很想和一个区块链经济机制感兴趣的人谈谈,如果他们拥有这个工具箱,他们会用来做什么?他们能做做出什么?你如果是这个兴趣者,有什么想法呢?

Isaac:当然可以。你所说的本质上是一种限制你的钱的使用方式的能力。这是一个通用的概念,你可以用它来做任何事情。我非常有兴趣想看看有人会用这个点子来完成什么。

Greg:是的。回到我们在开始提到的一点:这意味着您可以分析财务行为、交易行为的结构来进行估值。这种估值的概念是算法的形式得出的,而不再是由主观的社会共识来主导。

这不是一个魔术,这里没有一个反重力机器,不是从帽子里拉出一只兔子。直接基于估值体系的社会共识异常复杂,而基于交易行为本身的设计之上的社会共识要简单的多,这种复杂性会慢慢转移。如果每个人都遵守了游戏规则(交易行为的规则),那么估值就变得客观了。

Isaac:这让我想起了区块链,因为这基本上就是你正在做的事情。我们不再寄希望于相信人们会按照他们说的去做。现在我们把所有的都转换成可以执行和验证的代码,并确保它将以我们期望的方式运行。

Greg:完全正确。我可能不应该在公开场合说这个,但我会去参加这些以太坊会议,人们会说,“现在我们可以看一下代码,看看它到底会做什么。” 但我会犹豫,因为这个说法不对。确定一段代码是否会调用某个特定的子程序,这本身是个很难的停机问题。除非你有别的东西来确保这不会发生。

可以通过代码审核来说明我说的这个观点。Dao经过代码审核,但内部却有各种各样的漏洞。所有仅仅查看代码是不够的。

另一方面,人们长期以来一直认为,“好吧,任何验证到这个地步就做不下去了。” 不,不是这样的。有两个不同的表现力:语言本身的表现力,可验证的属性(译者注:“属性”这里指形式化验证的属性,比如一段代码无论怎样执行,都不会让余额变成负数,这就是一个“属性”)也有表现力,然后中间有个最佳点,在那个时候你同时可以在语言上获得有趣的表达力,也在程序的可以验证的属性集合上获得有趣的表达力。这时就足够涵盖大量的交易行为了。

如果人们真的想在数学上看到这一点,在Caires的“Pi演算的逻辑中的空间行为属性”中,他为Pi演算找出了一类模型检查会终止的公式(译者注:模型检查会终止,表示不会受到停机问题的困扰,会在确定时间内判断某个属性是否成立,即形式验证能够在确定时间内给出答案)。这是一个非常重要的经典公式。但你可以进一步改变它。你可以增加公式的能力,只要你同时相应地限制你的进程的能力,这实际上就是把你的脚本语言限制在一些更容易处理的级别上,来换得更有趣的可以验证的公式。(译者注:可以对脚本语言施加限制来换取更多的可以形式验证的 属性集)

这个思路会使得以太坊会议上的这些人所宣称的直觉(你可以查看代码弄懂它的行为)变得真正可行。他们只想通过人眼检查来做到这一点,这是永远不可能的。但是他们最求的目标,却是绝对可能的,通过类型信息可以做到这一点。如果我们使用这些概念来设计金融工具和数字货币,这是一个可行的方式,或者至少到目前为止,这似乎是最有效和最在数学层面可以掌控的方法。