Starlark是否为图灵完备语言及相关技术问题问询

缺少用户自定义数据类型、无限循环和递归三个特性，是否足以判定一门语言属于图灵不完备语言？ #

• 仅缺少无限循环和递归两个特性就足够判定图灵不完备，和是否支持自定义数据类型没有必然关联。
• 图灵完备的核心要求是可以模拟图灵机的任意状态转换，对应到编程语言层面必须具备执行任意长度计算的能力，该能力只能通过无界循环或无界递归实现。如果两者都被禁止，程序最多只能执行固定有限次操作，计算能力上限仅为有限状态自动机，远达不到图灵完备的要求。
• 自定义数据类型本质是语法层面的便利特性，哪怕仅支持内置的整数、字符串等基础类型，只要能实现无界循环/递归，依然可以达到图灵完备，比如极简编程语言Brainfuck没有自定义类型能力，但属于公认的图灵完备语言。

是否存在可以证明Starlark不具备图灵完备性的相关依据？ #

Starlark的官方规范里明确做了三类强制限制，直接证明其不满足图灵完备要求：

• 没有原生无限循环语法，仅有的for循环只能迭代有限长度的可迭代对象，不支持无固定终止条件的循环结构；
• 完全禁止递归调用，同时设置了硬编码的调用栈深度上限，超出上限会直接抛出运行错误；
• 所有内置操作的执行步数都是有界的，不存在可以无限执行的内置逻辑。
  以上限制决定了任何Starlark程序的总执行步数都是可预期的有限值，无法模拟需要任意长执行步骤的图灵机，自然不具备图灵完备性。

若一门语言不是图灵完备的，是否意味着其运行的所有程序都必然会最终终止？ #

这个推论不成立，属于常见的认知误区：

• 图灵不完备仅代表语言的计算能力弱于图灵机，无法模拟所有图灵可计算函数，和是否保证所有程序停机没有必然的反向推导关系。
• 举个简单的反例：假设设计一门极简语言，禁止递归，仅支持整数加减和while True无限循环语法，没有其他复杂逻辑，这门语言显然无法模拟完整图灵机（属于图灵不完备），但只要写一个空的while True语句就能无限运行不会终止。
• 反过来的推论才成立：如果一门语言可以保证所有程序必然终止（这类语言也被称为总语言，比如Coq、Agda的核心计算层），那它一定是图灵不完备的，因为图灵完备的语言必然存在无法判定是否停机的程序。

内容的提问来源于stack exchange，提问作者ams