У меня нет формального знания о продолжениях, и мне интересно, может ли кто-нибудь помочь мне проверить и понять код, который я написал:).
Проблема
Общая проблема, которую я пытаюсь решить, - это преобразовать выражения типа
(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?
Я слышал продолжение, описанное как "остальное вычисление", и подумал, что мне нужно. Следуя этой идее, a var должен взять функцию
f :: α -> E -- rest of computation
аргументом которого будет значение переменной var, созданное и возвращающее то, что мы хотим (обозначение кода, помеченное как result), новая функция, принимающая переменную x и возвращающую f x. Следовательно, определим,
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
ну, похоже, он работает.
