“在给定的二进制代码中查找所有代码等同于停机问题。”真的吗？
我刚读了一个关于模拟器的高票问题，其中有这样一句话： 已经被证明，找到给定二进制文件中所有代码与判断一段程序是否能终止的问题是等价的。 这句话真的让我印象深刻。 这难道是真的吗？难道它不只是一个大的依赖图吗？ 非常感谢对此声明提供更多深入见解。
自动和确定性地测试函数的结合律、交换律等性质。
是否可能构建一个高阶函数isAssociative，该函数接受另一个具有两个参数的函数，并确定该函数是否是结合性的？ 类似的问题也可以用于其他属性，例如交换律。 如果这是不可能的，是否有任何一种语言可以自动化实现？如果有Agda，Coq或Prolog解决方案，我很感兴趣。 我可以设想一种...
有没有“足够好”的解决停机问题的方法？
众所周知，停机问题无法有明确的解决方案，即a) 返回true 程序确实停机，b) 处理任何输入，但我想知道是否有足够好的解决方案来解决该问题，可以完美处理某些程序流程，或者能够识别出它不能正确解决问题的情况，或者在大多数情况下是正确的等等... 如果有，它们有多好，并且它们依赖于什么思想...
在C/C++代码中查找指针是否与停机问题静态等价？
我对静态代码分析的正式方面了解不深，因此有此问题。 几年前，我读到使用静态代码分析区分代码和数据等价于停机问题。 （需要引用，但我已经没有了。Stackoverflow在这里或这里有相关讨论。）至少对于基于冯·诺伊曼结构的常见计算机体系结构，在其中代码和数据共享相同的内存，这似乎是有道理的。...
Maybe类型的mfix函数是否不可能是非平凡总函数？
由于对于每个 f，都有 Nothing >>= f = Nothing，因此以下简单的定义适用于 mfix： mfix _ = Nothing 但这没有实际用途，因此我们有以下非全面的定义： mfix f = let a = f (unJust a) in a where ...
不可判定实例如何导致编译器崩溃？
当我第一次阅读关于-XUndecidableInstances的严肃批评时，我已经完全习惯了它，认为它只是为了让编译器更容易实现而消除了Haskell98必须遵守的烦人限制。 事实上，我遇到过很多需要使用不可判定实例的应用程序，但没有一个实际上与不可判定性相关的问题。卢克的例子之所以有问题，...