问题[functional-programming](coding)

我正在与 Dafny 合作，试图了解规范（特别是修改和确保多集）如何影响验证。

我有一个方法do_nothing，用于修改数组 a，但确保其元素的多集保持不变。该方法的主体为空。

method do_nothing(a: array<int>)
  modifies a
  ensures multiset(a[..]) == multiset(old(a[..]))
{
  // nothing is done
}

method test()
{
  var a := new int[6] [2, -3, 4, 1, 1, 7];
  assert a[..] == [2, -3, 4, 1, 1, 7]; // Verifies
  assert a[0] !=0 ;                    // Verifies

  do_nothing(a);

  assert a[0] != 0; // <-- Verification Error: This assertion cannot be proved
}

我的期望：

a由于其中根本没有 0 ，并且 dafny 同意do_nothing确保multiset(a[..]) == multiset(old(a[..]))。因此，断言 a[0] != 0 应该成立并验证成功。

问题：

Dafny 无法验证最终断言 assert a[0] != 0;

我对 Agda 很熟悉。我决定尝试一下 Lean，但我发现命题相等性真的让我很困扰。有时候我发现 rfl 能正常工作，但有时候却不行，原因我完全不明白，这真让人沮丧。举个例子：

inductive Λ where
  | var : String → Λ
  | app : Λ → Λ → Λ
  | abs : String → Λ → Λ
  deriving Repr, BEq, DecidableEq

def FV : Λ → HashSet String
  | Λ.var x => HashSet.ofList [x]
  | Λ.app m n  => FV m ∪ FV n
  | Λ.abs x m => (FV m).erase x
  
#eval FV (Λ.var "x")  -- Std.HashSet.ofList ["x"]
example : FV (Λ.var "x") = HashSet.ofList ["x"] := rfl  -- fine
example : (2 == 1 + 1) = true := rfl -- fine
#eval FV (Λ.var "x") == HashSet.ofList ["x"]  -- true
example : (FV (Λ.var "x") == HashSet.ofList ["x"]) = true := rfl
--type mismatch
--  rfl
--has type
--  ?m.9390 = ?m.9390 : Prop
--but is expected to have type
--  (FV (Λ.var "x") == HashSet.ofList ["x"]) = true : Prop

表达式的计算结果与预期一致，但在前两个例子中， rfl 运行良好，但在最后一个例子中却莫名其妙地不行，似乎没有减少 = 两边的项。我可以想象两个具有相同值的 HashSet 并不总是相等，因为它们可能最终位于不同的 bucket 中，但我不确定这是否是问题所在，因为它的计算结果似乎很好。

我是 OCaml 的新手，在理解模块类型如何工作方面有些困难。

module type I = sig
  type t
end

module EQ (M : I) = struct
  let equal (x : M.t) (y : M.t) = x = y
end

(* Explicitly type declaration *)
module A : I = struct
  type t = string
end

module EStr1 = EQ (A)

(* Error: This expression has type string but an expression was expected of type
         A.t *)
let _ = EStr1.equal "1" "0" |> string_of_bool |> print_endline

(* No type declaration *)
module B = struct
  type t = string
end

module EStr2 = EQ (B)

(* OK. Outputs false *)
let _ = EStr2.equal "1" "0" |> string_of_bool |> print_endline

在上面的代码中，我声明了模块类型I、具有显式模块类型声明的模块和没有模块类型声明的A模块。是接收类型模块并返回带有方法的模块的函子。BEQIequal

带有模块的示例A导致编译错误，而另一个示例则按我预期运行。这些示例之间的语义差异是什么？

我很难弄清楚我的 Idris2 类型错误或编译错误是什么，所以我想我可以请一些 Idris2 老手或爱好者给我一些解释，说明如何使我的方法有效，或者为什么它不能那样工作。任何额外的信息和深入的建议总是非常感激，因为我想利用这些知识将东西从 Haskell 转换为 Idris2，以获得可证明的结构等。

我已经知道的通用解决方案是这个（包含所有辅助函数）：

data Vect : (len : Nat) -> (a : Type) -> Type where
  Nil  : Vect 0 a
  (::) : (x : a) -> (xs : Vect n a) -> Vect (S n) a

zipWith : (a -> b -> c) -> Vect n a -> Vect n b -> Vect n c
zipWith f []        []         = []
zipWith f (x :: xs) (y :: ys)  = f x y :: zipWith f xs ys


replicate : (n : Nat) -> a -> Vect n a
replicate 0     _  = []
replicate (S k) va = va :: replicate k va

replicate' : {n : _} -> a -> Vect n a
replicate' = replicate n


transpose : {m : _} -> Vect n (Vect m a) -> Vect m (Vect n a)
transpose [] = replicate' []
transpose (xs::xss) = zipWith (::) xs (transpose xss)

这就是我正在学习的 GitHub 指南中的解决方案。

现在我的做法是：

transLines : Vect n (Vect (S m) a) -> Vect n a
transLines [] = []
transLines ((x :: _) :: xss) = x :: transLines xss

dropLines : Vect n (Vect (S m) a) -> Vect n (Vect m a)
dropLines [] = []
dropLines ((_ :: xs) :: xss) = xs :: dropLines xss


transpose' : {m : _} -> Vect n (Vect m a) -> Vect m (Vect n a)
transpose' {m = 0} [] = []
transpose' ([]:: _) = []
transpose' ma = (transLines ma) :: transpose' (dropLines ma)

我知道具体是什么不起作用，当我在转置函数中调用“droplines ma”时，“Vect n (Vect ma)”和“Vect ?n (Vect (S ?m) a)”的类型无法匹配，但这正是我遇到困难的地方，我不知道是否可以更改一些定义以使其起作用，或者整个方法是否不适用于依赖类型。

提前感谢您，祝您好运

我正在学习 OCaml，在函数式编程方面遇到了一些麻烦......

我需要创建一个函数，用于替换给定整数列表的字符，即字符串中该索引处的字符。例如，我输入 [1;4] 'u'“Hello”，它输出“Hullu”。

这就是我想出的：

let remplace_positions lst c str =
  let rec acc lst c str n l_index ret =
    match (n >= String.length str, List.nth lst l_index = n) with 
    | true, _ -> ret
    | _, true -> acc lst c (n+1) (l_index+1) (ret ^ (String.make 1 c))
    | _, _ -> acc lst c (n+1) (l_index+1) (ret ^ (String.make 1 (String.get str n)))
  in 
  acc lst c str 0 0 ""

但如您所见，最后两个匹配案例存在错误。它们是字符串 -> 字符串类型，但我希望它们是字符串类型。

有人知道如何在递归调用函数时修复这个问题吗？

我正在尝试剖析并理解可枚举协议中的工作acc/0原理。reducer/0

def map(enumerable, fun) do
  reducer = fn x, acc -> {:cont, [fun.(x) | acc]} end
  Enumerable.reduce(enumerable, {:cont, []}, reducer) |> elem(1) |> :lists.reverse()
end

有人可以从每个枚举中的 x、acc 的值开始解释这一点吗

这个表情

max([1]) + 1

给出

Unable to call: `+` with arguments: (`1 | Null`, `1`).
 Reasons:
    - Expecting Type: `Number`, but got: `Null`.
        |-- From: `Number`  
        |- From: +(lhs: Number, rhs: Number) -> Number      
            50| max([1]) + 1
                ^^^^^^^^
    - Expecting Type: `Array<T>`, but got: `Null`.
        |-- From: `Array<T>`    
        |- From: +<T, E>(lhs: Array<T>, rhs: E) -> Array<T | E>     
            50| max([1]) + 1
                ^^^^^^^^
    - 10 more options ...

50| max([1]) + 1
    ^^^^^^^^^^^^

但typeOf(max([1]))给出Number. 如何获取 max 的结果作为可用于数字运算的数字？

所以这是我在家庭作业中遇到的问题，我必须证明 bool 不等于 top，而且我必须使用一个重新定义的等号。

module TranspEq where

open import Agda.Primitive
open import Agda.Builtin.Equality renaming (_≡_ to _≡ᵣ_ ; refl to reflᵣ)
open import Agda.Builtin.Nat renaming (Nat to ℕ)

_≡_ : ∀{ℓ}{A : Set ℓ} → A → A → Setω
_≡_ {A = A} a b = ∀{κ}(P : A → Set κ) → P a → P b

infix 4 _≡_

-- define conversion between the two 'equals'
transp : ∀{ℓ}{A : Set ℓ}(a b : A) → a ≡ b → a ≡ᵣ b
transp a b x = x (_≡ᵣ_ a) reflᵣ

untransp : ∀{ℓ}{A : Set ℓ}(a b : A) → a ≡ᵣ b → a ≡ b
untransp a .a reflᵣ P y = y

-- prove properties of ≡

refl : ∀{ℓ}{A : Set ℓ}{a : A} → a ≡ a
refl P a = a

sym : ∀{ℓ}{A : Set ℓ}{a b : A} → a ≡ b → b ≡ a
sym {l} {A} {a} {b} = λ z P → z (λ z₁ → (x : P z₁) → P a) (λ x → x)

trans : ∀{ℓ}{A : Set ℓ}{a b c : A} → a ≡ b → b ≡ c → a ≡ c
trans = λ a b P c → b P (a P c)

cong : ∀{ℓ κ}{A : Set ℓ}{B : Set κ}(f : A → B){a b : A} → a ≡ b → f a ≡ f b
cong = λ f a P → a (λ b → P (f b))

-- types
record ⊤ : Set where
  instance constructor tt

data Bool : Set where
  true : Bool
  false : Bool

data ⊥ : Set where

_≢_ : ∀{ℓ}{A : Set ℓ} → A → A → Setω
a ≢ b = a ≡ b → ⊥

Bool≠⊤ : Bool ≢ ⊤
Bool≠⊤ = {!!}

我尝试了类似的方法，但是我无法成功：/无法创建 Set -> Set 谓词

⊤≠⊥ : ⊤ ≢ ⊥ 
⊤≠⊥ x = x (λ x → x) tt
 

Bool≠⊤ : Bool ≢ ⊤
Bool≠⊤ x = ⊤≠⊥ λ P y → {!   !}
--Bool≠⊤ : Bool ≢ ⊤
--Bool≠⊤ x = x (λ y → y tt) p
--    where
--    p : {Set : (Bool ≡ ⊤)}→ ⊥
--    p (true ≡ tt) = ⊥
--    p (false ≡ tt) = ⊥