与Coq相比,Isabelle/HOL证明助手是否有任何弱点和优势？
因为那里有非图灵完整的语言,并且鉴于我没有在大学学习Comp Sci,有人可以解释一下Turing-incomplete语言(如Coq)不能做的事情吗？
或者是没有实际利益的完整性/不完整性(即它在实践中没有太大的区别)？
编辑 - 我正在寻找一个答案,你不能用非Turing完整语言构建一个哈希表,因为X或类似的东西!
programming-languages functional-programming turing-complete coq
我想知道是否有人可以告诉我Z3和coq之间的区别？在我看来,coq是一个证明助手,因为它要求用户填写证明步骤,而Z3没有这个要求.但似乎coq也有类似于Z3的自动战术？或者也许coq中的证明搜索能力不如Z3强大？
我被告知在依赖类型系统中,"类型"和"值"是混合的,我们可以将它们都视为"术语".
但是有一些我无法理解的东西:在没有Dependent Type(如Haskell)的强类型编程语言中,在编译时决定(推理或检查)类型,但是在运行时决定(计算或输入)值.
我认为这两个阶段之间肯定存在差距.试想一下如果从STDIN以交互方式读取一个值,我们如何在必须决定AOT的类型中引用该值？
例如,我需要从STDIN中读取一个自然数n和一个自然数列表xs(包含n个元素),如何将它们放入数据结构中Vect n Nat？
forall n m : nat, exists q : nat, exists r : nat, n = q * m + rq并且是r从值m和n.Fixpoint并将其提取出来.我想仔细注意那个任务不是我在这里考虑的.甚至可以将我的证明中隐含的算法提取到Haskell中吗？如果有可能,怎么办呢？
假设我有一个任意的 Coq术语（使用s-expressions / sexp的AST格式），例如：
n = n + n
我想自动将其转换为：
= n + n n
通过遍历AST树（由于sexp，它是列表的嵌套列表）。Python中是否有可以执行此操作的标准库？
现在，如果我要写下要执行的算法/伪代码（假设我可以将sexp转换为某些实际的树对象）：
def ToPolish():
'''
"postfix" tree traversal
'''
text = ''
for node in root.children:
if node is atoms:
text := text + node.text
else:
text := text + ToPolish(node,text)
return text
我认为这很接近，但我认为某处存在一个小错误...
AST示例：
(ObjList
((CoqGoal
((fg_goals
(((name 4)
(ty
(App
(Ind
(((Mutind (MPfile (DirPath ((Id Logic) (Id Init) (Id Coq))))
(DirPath ()) (Id eq))
0)
(Instance ())))
((Ind
(((Mutind (MPfile (DirPath ((Id …[我不确定这是否适合堆栈溢出,但此处还有许多其他Coq问题,所以也许有人可以提供帮助.]
我正在从http://www.cis.upenn.edu/~bcpierce/sf/Basics.html#lab28处理以下内容(正好在Case的介绍下面).请注意,我是一个完全的初学者,我在家工作 - 我不是学生.
Theorem andb_true_elim1 : forall b c : bool,
andb b c = true -> b = true.
Proof.
intros b c H.
destruct b.
Case "b = true".
reflexivity.
Case "b = false".
rewrite <- H. reflexivity.
Qed.
我正在看重写的内容:
Case := "b = false" : String.string
c : bool
H : andb false c = true
============================
false = true
然后rewrite <- H.应用:
Case := "b = false" : String.string
c : …我想有一个归纳类型来描述排列及其对某些容器的行为.很明显,根据这种类型的描述,算法的定义复杂度(就其长度而言)(计算组合或逆,分解成不相交的循环等)将会变化.
考虑Coq中的以下定义.我认为这是Lehmer代码的形式化:
Inductive Permutation : nat -> Set :=
| nil : Permutation 0
| cons : forall (n k : nat), Permutation (k + n) -> Permutation (k + S n).
很容易在大小为n的向量上定义它的动作,在其他容器上稍微硬一些,并且(至少对我而言)很难找到组合的形式化或逆向.
或者,我们可以将置换表示为具有属性的有限映射.可以容易地定义组合或逆,但是将其分解成不相交的循环是困难的.
所以我的问题是:是否有任何文件可以解决这个权衡问题？我设法找到的所有工作都处理了命令式设置中的计算复杂性,而我对"推理复杂性"和函数式编程感兴趣.
我是依赖类型的新手,我对这两者之间的区别感到困惑.看来人们通常说一个类型是由其他类型的参数,并通过一定的价值索引.但是,依赖类型语言中的类型和术语之间没有区别吗？参数和指数之间的区别是否基本？你能告诉我在编程和定理证明中它们的含义不同的例子吗？
我在Coq的SSReflect扩展中找到了两个公约,这些公约看起来特别有用,但我还没有看到在新的依赖类型语言(Lean,Agda,Idris)中广泛采用的公约.
首先,可能的谓词表示为布尔返回函数,而不是归纳定义的数据类型.这默认带来可判定性,通过计算开辟了更多的证明机会,并通过避免校对引擎携带大量证明条件来提高检查性能.我看到的主要缺点是需要使用反射词来在证明时操纵这些布尔谓词.
其次,具有不变量的数据类型被定义为包含简单数据类型和不变量证明的从属记录.例如,固定长度序列在SSReflect中定义,如:
Structure tuple_of : Type := Tuple {tval :> seq T; _ : size tval == n}.
A seq和证明该序列的长度是一定值.这与Idris如何定义此类型相反:
data Vect : (len : Nat) -> (elem : Type) -> Type
一种依赖类型的数据结构,其中不变量是其类型的一部分.SSReflect方法的一个优点是它允许重用,因此例如许多定义的函数seq和关于它们的证明仍然可以使用tuple(通过对底层操作seq),而使用Idris的方法函数reverse,append等等需要被重写Vect.Lean实际上在其标准库中具有等效的SSReflect样式vector,但它也具有Idris样式array,似乎在运行时具有优化的实现.
一本面向SSReflect的书甚至声称Vect n A风格方法是反模式:
依赖类型语言和Coq中的常见反模式特别是将这样的代数属性编码到数据类型和函数本身的定义中(这种方法的规范示例是长度索引列表).虽然这种方法看起来很吸引人,因为它展示了依赖类型捕获它们的数据类型和函数的某些属性的能力,但它本质上是不可扩展的,因为总会有另一个感兴趣的属性,这是设计者没有预见到的.数据类型/函数的数据,因此它必须被编码为外部事实.这就是为什么我们提倡这种方法,其中数据类型和函数被定义为尽可能接近程序员定义的方式,并且它们的所有必要属性都是分开证明的.
因此,我的问题是,为什么没有更广泛地采用这些方法.我缺少哪些缺点,或者它们的优势在具有比Coq更好支持依赖模式匹配的语言中不那么重要？