标签: proof

有谁知道以下任何例子？

1. 关于证明助理(例如Coq)中正则表达式(可能通过反向引用扩展)的证据开发.
2. 关于正则表达式的依赖类型语言(例如Agda)中的程序.

在这个关于NP,NP-hard和NP-complete定义的问题的答案中,Jason提出了这样的主张

停止问题是经典的NP难问题.这是给出程序P和输入I的问题,它会停止吗？这是一个决策问题,但它不在NP中.很明显,任何NP完全问题都可以简化为这个问题.

虽然我同意停止问题在直觉上比NP中的任何问题都要困难得多,但老实说,我无法提出一个正式的数学证明,即停止问题是NP难的.特别是,我似乎无法找到从NP(或至少任何已知的NP完全问题)中的每个问题的实例到停止问题的多项式时间多对一映射.

是否有一个直截了当的证据表明停止问题是NP难的？

当我们开始进入算法设计和更多离散的计算机科学主题时,我们最终必须一直在证明事物.每当我看到有人问如何变得非常擅长证明时,常见的(也可能是懒惰的)答案就是"练习".

如果你掌握了基础知识,那么练习就没有问题,但是你如何进入数学证明的思维定势？什么时候感应点击？哪些资源最适合教授这些主题？在沉迷于校对之前,应该研究哪些基础课题？

在Idris/Haskell中,可以通过注释类型和使用GADT构造函数来证明数据的属性,例如使用Vect,但是,这需要将属性硬编码到类型中(例如,Vect必须是与List不同的类型).是否可以使用具有开放属性集的类型(例如包含长度和运行平均值的列表),例如通过重载构造函数或使用效果的静脉？

Martin Fowler 有一个Money类,有一个货币分配程序.该例程根据给定的比率列表分配资金,而不会通过舍入而损失任何价值.它会将任何余数值传播到结果上.

例如,由"比率"(1,1,1)分配的100美元将产生(34美元,33美元,33美元).

这是allocate功能:

public long[] allocate(long amount, long[] ratios) {
    long total = 0;
    for (int i = 0; i < ratios.length; i++) total += ratios[i];

    long remainder = amount;
    long[] results = new long[ratios.length];
    for (int i = 0; i < results.length; i++) {
        results[i] = amount * ratios[i] / total;
        remainder -= results[i];
    }

    for (int i = 0; i < remainder; i++) {
        results[i]++;
    }

    return results;
}

(为了这个问题,为了简单起见,我冒昧地用long取代Money类型.)

问题是,我怎么知道它是正确的？除了最终的for-loop之外,这一切似乎都是不言而喻的.我认为,为了证明函数是正确的,在最终的for循环中证明以下关系是正确的就足够了:

remainder < …

可以从n个不同的元素构造多少个二叉搜索树？我们怎样才能找到一个经过数学验证的公式呢？

示例: 如果我们有3个不同的元素,比如说1,2,3,则有5个二叉搜索树.

我试图证明,我的想法是一个合理的定理:

theorem1 : (n : Nat) -> (m : Nat) -> (n + (m - n)) = m

通过归纳证明达到了我需要证明这一点的程度:

lemma1 : (n : Nat) -> (n - 0) = n

当我尝试使用交互式证明器证明它(引理,为简单起见)时会发生这种情况:

----------                 Goal:                  ----------
{hole0} : (n : Nat) -> minus n 0 = n

> intros
----------              Other goals:              ----------
{hole0}
----------              Assumptions:              ----------
 n : Nat
----------                 Goal:                  ----------
{hole1} : minus n 0 = n

> trivial
Can't unify
        n = n
with
        minus n 0 = …

import Prelude hiding (foldr)

import Control.Applicative
import Data.Foldable
import Data.Traversable

left, right :: (Applicative f, Traversable t) => (a -> b -> b) -> b -> t (f a) -> f b
left f z = fmap (foldr f z) . sequenceA
right f z = foldr (liftA2 f) (pure z)

我强烈怀疑左右表达是否相等,但如何证明呢？

在编写数学证明时,一个目标是继续压缩证明.证明变得更优雅,但不一定更具可读性.压缩意味着更好的理解,因为你清除了不必要的字符和冗长.

我经常听到开发人员说你应该让代码足迹尽可能小.这可以非常快速地产生不可读的代码.在数学方面,这不是一个问题,因为这个练习纯粹是学术性的.然而,在时间就是金钱的生产代码中,让人们试图弄清楚一些非常简洁的代码正在做什么似乎没有多大意义.对于更详细的代码,您可以获得可读性和节省.

你什么时候停止压缩软件代码？

以下代码是Idris:

natAssociative : (a : Nat) -> (b : Nat) -> (c : Nat) -> (a + b) + c = a + (b + c)
natAssociative Z b c = the (b + c = b + c) refl
natAssociative (S k) b c = replace {P=\x => S (k + b) + c = S x} (natAssociative k b c) refl

我正在艰难地将其转化为无形.我尝试了一些不同的编码,但我认为这是最有希望的开始:

import scalaz.Leibniz._
import shapeless.{ HNil, Nat, Succ, Poly3 }
import shapeless.Nat._
import shapeless.ops.nat._

object natAssociative extends …