当参数表明结果不应该存在时的依赖型设计

如何解决当参数表明结果不应该存在时的依赖型设计

这是对 my previous question on dependently-typed arbitrarily-dimensioned matrices 的跟进。

我定义了一个矩阵类型，其中 dims 中的每个自然定义了相应维度的大小。例如，对于某些类型 A，matrix A [3; 5; 2] 是一个 3x5x2 矩阵：

Require Import Coq.Unicode.Utf8.
Require Export Vector.
Import VectorNotations.
Require Import List.
Import ListNotations.

Fixpoint matrix (A: Type) (dims: list nat) :=
  match dims with
  | [] => A
  | head::tail => Vector.t (matrix A tail) head
  end.

我还定义了一个 get 函数，它在指定所有索引时访问矩阵的元素：

Fixpoint get {A: Type} {dims: list nat} (m: matrix A dims) (indexes: list nat): option A :=
  if Nat.eqb (length dims) (length indexes)
  then match dims,indexes return matrix A dims → option A with
       | [],[] => λ a,Some a
       | dimh::dimt,idxh::idxt => λ m',match Fin.of_nat (idxh - 1) dimh with
           | inleft H => @get A dimt (Vector.nth m' H) idxt
           | _ => None
           end
       | _,_ => λ _,None
       end m
  else None.

现在我想支持 MATLAB 样式的索引器，其中索引是标量或范围；特殊范围 : 表示“该维度中的所有相应元素”。此函数不需要处理 MATLAB 仅指定一些索引的能力；我们将假设提供了所有索引。一些例子：

>> A = rand(3,5,2)

A(:,:,1) =

    0.8147    0.9134    0.2785    0.9649    0.9572
    0.9058    0.6324    0.5469    0.1576    0.4854
    0.1270    0.0975    0.9575    0.9706    0.8003


A(:,2) =

    0.1419    0.7922    0.0357    0.6787    0.3922
    0.4218    0.9595    0.8491    0.7577    0.6555
    0.9157    0.6557    0.9340    0.7431    0.1712

>> size(A)

ans =

     3     5     2

>> A(1,1,1)

ans =

    0.8147

>> A(1,:)       

ans(:,1) =

    0.8147


ans(:,2) =

    0.1419

>> A(1,2:4,:)

ans(:,1) =

    0.9134    0.2785    0.9649


ans(:,2) =

    0.7922    0.0357    0.6787

我可以定义表示索引器的类型：

Inductive range: Type :=
  | Scalar: nat → range
  | Subrange: nat → nat → range
  | Fullrange.

但我正在努力的地方是计算函数的结果类型。我最初的想法是定义一个函数 range_dimensions: list nat -> list range -> list nat 的想法是范围列表中的每个标量给出一个 1 的维度，每个子范围给出一个子范围大小的维度，每个完整的-range 给出维度列表对应大小的维度（第一个参数）。

但是，当列表的大小不同，或者子范围的一部分超出范围（例如，Subrange 3 5 表示大小为 4 的维度）时，返回不是一个好结果——换句话说，我更喜欢range_dimensions: list nat -> list range -> option (list nat)。但这提出了如何处理实际索引功能的问题：

Fixpoint get_range {A: Type} {dims: list nat} (m: matrix A dims) (indexes: list range): matrix A (range_dimensions dims indexes)

这行不通，因为类型不对齐。我真正想要的是返回一个 option (matrix A (range_dimensions dims indexes))，当维度计算失败时返回 None，否则返回 Some …，但我看不出有什么方法可以做到这一点。当维度列表为 option (matrix A …) 时，没有类型可用于 None：

Axiom range_dimensions_ex: option (list nat)
Check match range_dimensions_ex with
      | Some dims => matrix nat dims
      | None => option (matrix nat ???)
      end.

我认为这意味着我被我在 Certified Programming with Dependent Types 中看到的东西困住了，那就是使用类似

Fixpoint get_range {A: Type} {dims: list nat} (m: matrix A dims) (indexes: list range):
match (range_dimensions dims indexes) with
| None => unit
| Some dims' => matrix A dims'
end

这似乎很难处理，尤其是考虑到到目前为止我的其他矩阵函数返回 option (matrix A …) 来表示索引失败，而不是 tt。

我是不是找错了树？有没有更准确地反映我的目标的设计？请注意，这是为了将其用于 MATLAB 语义的（非常小的）子集的表达式评估函数中——如果我坚持使用 unit，否则我如何与返回 {{ 1}}？

解决方法

在 Coq 中编程的一种通用方法是将依赖类型限制在规范中，而不是在程序中使用它们。

因此，例如，矩阵可以表示为嵌套递归类型中的一对维度及其内容

Inductive matrix_ :=
| Scalar : scalar -> matrix_
| Matrix : list matrix_ -> matrix_
.

Record matrix :=
  { dim : list nat
  ; contents : matrix_
  }.

然后你需要一些谓词来指定矩阵何时是“格式良好”的：

Definition well_formed : matrix -> Prop := ...

操作将具有简单的类型：

Definition submatrix : matrix -> range -> matrix := ...

所有的复杂性都转移到规范中：

Theorem submatrix_wf (m : matrix) (r : range)
  : well_formed m -> valid_range m r -> well_formed (submatrix m r).

Theorem submatrix_dim (m : matrix) (r : range)
  : well_formed m -> valid_range m r -> dim (submatrix m r) = dim_range r.

(* etc. *)

这是一个简单的表示
在格式错误的输入中，您可以简单地返回垃圾而无需显式 option（而对于更结构化的表示，甚至可能没有“垃圾”的空间）；如果您验证您的程序，就会发现错误。
您仍然可以获得静态类型的许多好处：不会混淆矩阵、标量、布尔值、维度...

主要的权衡是使用依赖类型的丰富表示免费提供格式良好的证明，但让程序进行类型检查可能是一项非常困难的任务。使用愚蠢的表示，您只能从程序本身获得最基本的健全性检查（仍然比实际的 MATLAB 多）。但是，自动化可以在很大程度上减轻单独证明的繁琐。

当参数表明结果不应该存在时的依赖型设计

如何解决当参数表明结果不应该存在时的依赖型设计

解决方法

相关推荐