2

给定以下功能：

let rec foo l1 l2 = 
    match (l1,l2) with
        ([],ys) -> ys
      | (x::xs,ys) -> foo xs (x::ys))

证明以下性质：

  • foo (foo xs ys) zs = foo ys (xs@zs)

到目前为止，我已经完成了基本案例和归纳案例，但不知道如何开始证明：

基本情况：

  • foo (foo [] ys) zs = foo ys ([]@zs)
  • foo ys zs = foo ys zs

归纳案例：

  • foo (foo (x::xs) ys) zs = foo ys ((x::xs)@zs)
4

1 回答 1

1

以下是您要询问的证明类型的概述。我包括了基本情况。归纳案例留给您。确保在归纳案例的某处使用大纲中提到的假设来完成它。我=用于“平等”和=>评估。我不知道在您的上下文中可以使用哪些关系，您可以对评估和平等假设什么，或者您是否可以使用引理@或有可用的抽象定义。因此，您可能必须对此进行修改。

对 的结构进行归纳证明xs。

案例xs = []：：

foo (foo xs ys) zs
  =  foo (foo [] ys) zs          (* structure of xs *)
  => foo (match ([], ys) with ([], ys) -> ys | (* ... *)
                                 (* def. of foo, substitution *)
  => foo (ys) zs                 (* eval. of match *)
  =  foo ys zs                   (* drop parentheses *)
  =  foo ys ([] @ zs)            (* abstract def. of @ *)
  =  foo ys (xs @ zs)            (* structure of xs *)

案例xs = x::xs'：：

在这里，假设对于所有ys, zs, foo (foo xs' ys) zs = foo ys (xs' @ zs)。（这就是所谓的归纳假设。）

foo (foo xs ys) zs
  =  foo (foo (x::xs') ys) zs    (* structure of xs *)
  =  foo (match (x::xs', ys) with (* ... *) | (x::xs', ys) -> (* ... *)
                                 (* def. of foo, substitution *)
  => foo (foo xs' (x::ys)) zs    (* eval. of match *)

    (* for you *)

  =  foo ys ((x::xs') @ zs)      (* by some argument from you *)
  =  foo ys (xs @ zs)            (* structure of xs *)

如您所见，证明首先选择一个值进行结构归纳（您已经xs在问题中选择了）。然后，根据xs可能构造的所有可能方式将证明拆分为案例。由于xs大概是一个列表（这就是类型信息很重要的原因），它可能只有两种：它可能是[]，或者它可能是x::xs'某个值x和 list xs'。这分别导致基本情况和归纳情况。在这两种情况下，我们都必须证明相同的原始属性，但我们知道关于xs外观的额外信息（即 的“结构” xs）。

对于每种情况，您都使用该结构来找出您想要得到的陈述（在您的原始问题中大致正确）。然后，您尝试简单地从语句左侧的表达式转到右侧的表达式，使用评估规则、标识和任何可用的引理。在归纳的情况下，您还有一个可以使用的附加事实xs'（“归纳假设”）。这种“直接”的方法并不适用于研究层面的所有（也许是大多数）案例，但它适用于这个练习。

案例中证明的实际陈述是

  1. 如果xs = [], foo (foo xs ys) zs = foo ys (xs @ zs); 和
  2. 如果xs = x::xs'和foo (foo xs' ys) zs = foo ys (xs' @ zs)，那么foo (foo xs ys) zs = foo ys (xs @ zs)。

ys并且zs被隐含地普遍量化。

于 2016-02-04T19:02:30.113 回答