は、私は（カレーは、（F））ML

Question

を使用して、F、カレー（uncurry（G））= Gを=私は2つのML機能

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

を持っていると私は

uncurry(curry(f)) = f 

を証明したいuncurry証明したいです

と

curry(uncurry(g)) = g 

私は、検索エンジンのサイトを検索し、何も私を満足していません。 このテキストの先頭にある2つの機能は明確に定義されていません。例えば、uncurry（curry（f））= fを証明するには、カレー関数（fun curry f x y = f（x、y）;）を使用する必要がありますが、明確に定義されたカレーはありません。 2つのことを証明する方法は？

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が伸び意味で等しい機能（私たちは、機能extensionality公理を受け入れ、より多くの詳細がhere見つけることができます