我知道这与编程没有直接关系,但我想知道是否有人知道如何将泵浦引理应用于以下证明:
证明L = {(a ^ n)(b ^ n)(c ^ m):n!= m}不是无上下文语言
我对使用抽吸引理非常有信心,但这个真的让我感到厌烦.你怎么看？
我最近已经阅读了很多关于Haskell的内容,以及它作为一种纯函数式语言所带来的好处.(我对讨论Lisp的monad不感兴趣)对我来说(至少在逻辑上)尽可能地隔离具有副作用的函数是有意义的.我已经充分使用了setf其他破坏性功能,并且我认识到它们在Lisp和(大多数)其衍生物中的需要.
开始了:
(declare pure)可能帮助优化编译器？或者这是一个有争议的问题,因为它已经知道了？我很感激这里有任何见解.欢迎提供有关编译器实现或可证明性的信息.
编辑
为了澄清,我不打算将这个问题限制在Common Lisp中.它显然(我认为)不适用于某些衍生语言,但我也很好奇其他Lisps的某些功能是否倾向于支持(或不支持)这种设施.
lisp computer-science proof compiler-optimization purely-functional
假设我想证明以下定理:
Theorem succ_neq_zero : forall n m: nat, S n = m -> 0 = m -> False.
这个是微不足道的m,因为假设不能同时为后继和零.但是我发现证明这一点非常棘手,而且我不知道如何在没有辅助引理的情况下制作它:
Lemma succ_neq_zero_lemma : forall n : nat, O = S n -> False.
Proof.
intros.
inversion H.
Qed.
Theorem succ_neq_zero : forall n m: nat, S n = m -> 0 = m -> False.
Proof.
intros.
symmetry in H.
apply (succ_neq_zero_lemma n).
transitivity m.
assumption.
assumption.
Qed.
我很确定有更好的方法来证明这一点.最好的方法是什么？
如何在Coq中证明（forall x，P x / \ Q x）->（forall x，P x）？尝试了几个小时，无法弄清楚如何将前项分解为Coq可以消化的内容。（显然，我是新手：）
首先,这只能在没有副作用的算法上实现吗？
其次,我在哪里可以了解这个过程,任何好书,文章等？
我知道关系n = Big-O(1)是假的.但是,如果我们使用涉及Big-O的归纳法,则可以证明.但谬论是我们无法引入Big-O.但我的问题是我们如何通过使用常数来反驳这种关系.
这里有错误的证据,请使用常数给我证明它是假的.我对常量感到困惑,我不知道证明中使用的每个关系是否具有不同的常数或相同.请指教一下这个话题.
TO prove: n= O(1)
for n=1 , 1= O(1) proved
归纳假设:确实如此:n-1 = O(1)现在我们证明n = O(1)
LHS : n = (n-1) + 1
= O(1) + 1
= O(1) + O(1)
= O(1)
虚假证明..我想用<=和常量来澄清谬误,这是Big-O的基本定义.
我正在学习问题中的引理之间的区别.我能找到的每个引用都使用了这个例子:
{(a^i)(b^j)(c^k)(d^l) : i = 0 or j = k = l}
显示两者之间的差异.我可以找到一个使用常规引理来"反驳"它的例子.
选择w = uvxyz,st | vy | > 0,| vxy | <= p.假设w包含相等数量的b,c,d's.
我选择了:
u,v,x = ?
y = (the string of a's)
z = (the rest of the string w)
抽取y只会增加a的数量,如果| b | = | c | = | d | 起初,它现在还会.
(类似的论据,如果w没有a.那么只需抽出你想要的任何东西.)
我的问题是,奥格登的引理如何改变这一策略？"标记"有什么作用？
谢谢!
Isabelle/HOL验证器的核心算法是什么？
我正在寻找一个计划水平评估员的水平.
我只对Verifier感兴趣,而不是自动定理证明的策略.
我想从头开始实现一个简单的验证验证器(纯粹出于教育原因,而不是用于生产用途.)
我想了解Isabelle/HOL 的核心Verifier算法.我不关心用于自动定理证明的策略/代码.
我怀疑核心Verifier算法非常简单(而且优雅).但是,我找不到它.
谢谢!
到目前为止,我在Isabelle的以下风格中使用矛盾来编写证据(使用Jeremy Siek的模式):
lemma "<expression>"
proof -
{
assume "¬ <expression>"
then have False sorry
}
then show ?thesis by blast
qed
有没有一种方法可以在没有嵌套的原始校样块的情况下工作{ ... }？
因此,有一种被称为"折叠的普遍属性"的东西,完全如下:
g [] = i; g (x:xs) = f x (g xs) <=> g = fold f i
但是,正如您现在可能的那样,有一些罕见的情况dropWhile,fold f i 除非您将其概括,否则无法重新定义.
最简单但最明显的推广方法是重新定义通用属性:
g' y [] = j y; g' y (x:xs) = h y x xs (g' y xs) <=> g' y = fold (?) l
在这一点上,我可以做出我的假设:我假设存在某种功能p :: a -> b -> b,这将满足等式g' y = fold p l.让我们尝试用普遍属性帮助解决给定的方程式,一开始就提到:
g' y [] = j y = fold p l [] = l …haskell functional-programming proof generic-programming fold