静态输入语言意味着什么？

Question

我的理解是,这意味着可以编写一个程序来正式证明用静态类型语言编写的程序将没有某些(小)缺陷子集.

我的问题如下:

假设我们有两种图灵完整语言,A和B.A被认为是'类型安全'而'B'被假定为不是.假设我有一个程序L来检查用A写的任何程序的正确性.什么阻止我将用B写的任何程序翻译成A,应用L.如果P从A转换为B,那么为什么不是PL a用B编写的任何程序的有效类型检查器？

我接受过代数培训,而且我才刚开始学习CS,所以可能有一些明显的原因,这不起作用,但我非常想知道.整个'类型安全'的东西已经有一段时间闻到了我的味道.

Answer 1

如果你可以将每个 B'(用B编写的程序)翻译成等效的A'(如果B'是正确的话),则语言B享有与语言A一样多的"类型安全性"(在理论意义上,当然;-) - 基本上这意味着B是这样你可以做完美的类型推理.但这对动态语言来说非常有限 - 例如,考虑:

if userinput() = 'bah':
    thefun(23)
else:
    thefun('gotcha')

其中thefun(让我们假设)是int参数的类型安全,但不是str参数.现在 - 你怎么把它翻译成语言A呢？

Answer 2

让A成为你的图灵完备语言,它应该是静态类型的,当你删除类型检查时,让A'成为你从A得到的语言(但不是类型注释,因为它们也用于其他目的).接受的A程序将是A'公认程序的一部分.所以特别是A'也将是图灵完整的.

鉴于您的翻译P从B到A(反之亦然).该怎么办？它可以做两件事之一:

1. 首先,它可以将B的每个程序y转换为A的程序.在这种情况下,LPy将始终返回True,因为A的程序按定义正确键入.

2. 其次,P可以将B的每个程序y转换为A'的程序.在这种情况下,如果Py恰好是A的程序,则LPy将返回True,否则返回False.

由于第一种情况没有产生任何有趣的东西,让我们坚持第二种情况,这可能是你的意思.在B程序中定义的函数LP是否告诉我们关于B程序的任何有趣内容？我说不,因为它在P的变化下不是不变的.因为A是图灵完全的,即使在第二种情况下,P也可以被选择,使得它的图像恰好位于A.然后LP将一直是真的.另一方面,可以选择P,使得一些程序被映射到A'中的A的补码.在这种情况下,LP会为B的某些(可能是所有)程序吐出False.正如您所看到的,您没有得到任何仅依赖于y的东西.

我还可以通过以下方式更加数学化:编程语言的C类,其对象是编程语言,其态射是从一种编程语言到另一种编程语言的翻译.特别是如果存在态射P:X - > Y,则Y至少与X一样具有表现力.在每对图灵完备语言之间,在两个方向上都存在态射.对于C的每个对象X(即对于每种编程语言),我们有一个相关的集合,比如那些可以由X的程序计算的部分定义函数的{X}(坏符号,我知道).每个态射P:X - > Y然后诱导包含{X} - > {Y}的集合.让我们正式颠倒所有那些诱导身份{X} - > {Y}的态射P:X - > Y. 我将调用结果类别(用数学术语表示,由C'定位C).包含A - > A'是C'中的态射.然而,它不是在A'的自同构下保留的,即态射A - > A'不是C'中A'的不变量.换句话说:从这个抽象的角度来看,"静态类型"属性不是可定义的,可以任意地附加到语言上.

为了使我的观点更加清晰,你还可以将C'视为三维空间中几何形状的类别,同时将欧几里德运动视为态射.A'和B是两个几何形状,P和Q是欧几里德运动,将B带到A',反之亦然.例如,A'和B可以是两个球体.现在让我们在A'上修一个点,它代表A'的子集A. 让我们称这一点为"静态打字".我们想知道B的点是否是静态类型的.所以我们采取这样一个点y,通过P映射到A'并测试,它是否是我们在A'上的标记点.正如人们可以很容易看到的那样,这取决于所选择的地图P,换句话说:球体上的标记点不会被该球体的自同构(即将球体映射到自身的欧几里德运动)保留.