我刚刚写了一个延续吗？

Question

我没有正式的延续知识,我想知道是否有人可以帮助我验证和理解我写的代码:).

问题

我试图解决的一般问题是转换表达式

(2 * var) + (3 * var) == 4

进入功能

\x y -> 2 * x + 3 * y == 4 -- (result)

然后可以将其传递到yices-painless包中.

动机

作为一个更简单的例子,请注意将var其翻译成\x -> x.我们怎样才能乘两个var的(表示他们\x -> x和\y -> y)到一个表达\x -> \y -> x * y？

我听说延续被描述为"计算的其余部分",并认为这就是我所需要的.遵循这个想法,var应该采取一种功能

f :: ? -> E -- rest of computation

其参数将是创建的变量的值var,并返回我们想要的内容(代码列表标记result),一个新函数接受变量x并返回f x.因此,我们定义,

var' = \f -> (\x -> f x)

然后,对于乘法,比如xf和yf(例如,可能等于var),我们想要采用f :: ? -> E如上所述的"其余计算"函数,并返回一个新函数.我们知道函数应该使用和(表示和下面)的值来做什么,并将其定义为如此,xfyfxy

mult xf yf = \f -> xf (\x -> yf (\y -> f (x Prelude.* y)))

码

const' c = \f -> f c
var' = \f -> (\x -> f x) -- add a new argument, "x", to the function
add xf yf = \f -> xf (\x -> yf (\y -> f (x Prelude.+ y)))
mult xf yf = \f -> xf (\x -> yf (\y -> f (x Prelude.* y)))

v_? = var' -- "x"
v_? = var' -- "y"
v_? = var' -- "z"
m = mult v_? v_? -- "x * y"
a = add m v_? -- "x * y + z"
eval_six = (m id) 2 3
eval_seven = (a id) 2 3 1

two = const' 2 -- "2"
m2 = mult two v_? -- "2 * z"
a2 = add m m2 -- "x * y + 2 * z"
eval_two = (m2 id) 1
eval_eight = (a2 id) 2 3 1

quad_ary = (var' `mult` var') `mult` (var' `mult` var')
eval_thirty = (quad_ary id) 1 2 3 5

好吧,它似乎工作.

Answer 1

是的，这是用连续传递风格（CPS）编写的。

有人曾经向我解释延续性为“无处不在的回调”，我觉得这不是特别有用，但也许你会的。

就像很多事情一样，你能做的最好的事情可能就是继续努力，以更加流畅地运用这种风格。