Я только что написал продолжение?

У меня нет формальных знаний о продолжениях, и мне интересно, может ли кто-нибудь помочь мне проверить и понять код, который я написал :).

Проблема

Общая проблема, которую я пытаюсь решить, состоит в том, чтобы преобразовать выражения вроде

(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 и возвращает fx .Следовательно, мы определяем

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

. Затем для умножения, скажем, xf и yf (что может быть равно var , например), мы хотим чтобы взять функцию «остаточных вычислений» f :: α -> E , как указано выше, и вернуть новую функцию. Мы знаем, что должна делать функция, учитывая значения из xf и yf (обозначенные ниже x и y ] ), и определите это так,

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

ну, похоже, это работает.