У меня нет формальных знаний о продолжениях, и мне интересно, может ли кто-нибудь помочь мне проверить и понять код, который я написал:).
Проблема
Общая проблема Япопытка решить - преобразовать выражения типа
(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, как указано выше, и вернуть новую функцию.Мы знаем, что должна делать функция, учитывая значения из 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
ну вроде бы работает.