“通过将期望的结果与参数列表配对来定义的有限列表上的任何函数总是可以根据折叠” [英] "Any function on finite lists that is defined by pairing the desired result with the argument list can always be redefined in terms of fold"

问题描述

我正在阅读一篇有关普遍性和
折叠表达性的教程，并且卡在关于生成元组的部分。在显示 dropWhile 的常规定义如何不能用fold定义之后，使用元组定义 dropWhile 的例子是证明：

  dropWhile ::（a  - > Bool） - > [a]  - > [a] 
 dropWhile p = fst。 （dropWhilePair p）
 
 dropWhilePair ::（a  - > Bool） - > [a]  - > （[a]，[a]）
 dropWhilePair p = foldr fv 
其中
fx（ys，xs）=（if px then ys else x：xs，x：xs）
v =（[]，[]）
  

该文件指出：

事实上，这个结果是一个
一般定理（Meertens，1992）的一个实例，它指出了在
定义的有限列表上的任何函数通过将期望的结果与参数列表配对，总是可以根据折叠重新定义
，尽管不总是以不使用原始的
（可能是递归的）函数定义的方式。 / p>

我看了 Meerten的论文，但没有背景（类别理论？类型理论？），并没有完全发现这是如何被证明的。

有一个相对简单的证明为什么是这种情况？或者只是一个简单的解释，为什么我们可以用折叠的方式重新定义有限列表上的所有函数，如果我们将结果与原始列表配对即可。 解决方案 div>

考虑到你可以/可能需要使用里面的原始函数，你的问题中提到的索赔对我来说似乎是微不足道的：

  rewriteAsFold ::（[a]  - >（b，[a]）） - > [a]  - > （b，[a]）
 rewriteAsFold g = foldr fv其中
fx〜（ys，xs）=（fst（g（x：xs）），x：xs）
v =（fst （g []），[]）
  

编辑：添加〜，之后它似乎也适用于无限列表。

I was reading through the paper A tutorial on the universality and expressiveness of fold, and am stuck on the section about generating tuples. After showing of how the normal definition of dropWhile cannot be defined in terms of fold, an example defining dropWhile using tuples was proved:

dropWhile :: (a -> Bool) -> [a] -> [a]
dropWhile p = fst . (dropWhilePair p)

dropWhilePair :: (a -> Bool) -> [a] -> ([a], [a])
dropWhilePair p = foldr f v
  where
    f x (ys,xs) = (if p x then ys else x : xs, x : xs)
    v           = ([], [])

The paper states:

In fact, this result is an instance of a general theorem (Meertens, 1992) that states that any function on finite lists that is defined by pairing the desired result with the argument list can always be redefined in terms of fold, although not always in a way that does not make use of the original (possibly recursive) definition for the function.

I looked at Meerten's Paper but do not have the background (category theory? type theory?) and did not quite find how this was proved.

Is there a relatively simple "proof" why this is the case? Or just a simple explanation as to why we can redefine all functions on finite lists in terms of fold if we pair the results with the original list.

解决方案

Given the remark that you can / may need to use the original function inside, the claim as stated in your question seems trivial to me:

rewriteAsFold :: ([a] -> (b, [a])) -> [a] -> (b, [a])
rewriteAsFold g = foldr f v where
    f x ~(ys,xs) = (fst (g (x:xs)), x:xs)
    v            = (fst (g []), [])

EDIT: Added the ~, after which it seems to work for infinite lists as well.

这篇关于“通过将期望的结果与参数列表配对来定义的有限列表上的任何函数总是可以根据折叠”的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！