我想用ML证明uncurry(curry(f)) = f，curry(uncurry(g)) =g

Question

我有两个ML函数

fun curry f x y = f(x, y);
fun uncurry g (x, y) = g x y;

我想证明

uncurry(curry(f)) = f

和

curry(uncurry(g)) = g

我搜索了搜索引擎网站，但没有什么能让我满意。位于本文顶部的两个函数没有明确定义。例如，为了证明uncurry( curry (f)) =f，我必须使用curry函数(fun curry f x y= f(x，y);)，但是没有明确定义curry。如何证明两件事？

Answer 1

我将演示如何演示curry (uncurry f) = f。

curry (uncurry f) =                       (* by definition of uncurry *)
curry (fn (x,y) -> f x y) =               (* by definition of curry *)
fn x y -> ((fn (x,y) -> f x y) (x,y)) =   (* beta-reduction on innermost level *)
fn x y -> (f x y) =                       (* by eta-expansion *)
f

另一个问题也可以类似地解决。

注意:函数curry (uncurry f)和f在外延意义上是相等的(我们接受函数外延性公理，更多细节可以在here中找到。