ATS - Что означает ограничение C3NSTRprop (C3TKmain (); S2Eeqeq (S2Eintinf (0); S2Evar (abc (4303))))?

Question

У меня есть следующий код ATS:

extern prfun mul_nx0_0 {n:int} (): MUL(n, 0, 0)

extern prfun mul_nx1_n {n:int} (): MUL(n, 1, n)

extern prfun mul_neg_1 {m,n,p:int} (MUL(m, n, p)): MUL(~m, n, ~p)

extern prfun mul_neg_2 {m,n,p:int} (MUL(m, n, p)): MUL(m, ~n, ~p)

extern prfun mul_assoc {a,b,c,ab,bc,abc:int}
( MUL(a, b, ab)
, MUL(b, c, bc)
, MUL(ab, c, abc)
): MUL(a, bc, abc)

primplmnt mul_assoc {a,b,c,ab,bc,abc:int} (pf1, pf2, pf3) =
let
    prfun mul_assoc1 {a,b,c,ab,bc,abc:nat} .<a>.
    (pf1: MUL(a, b, ab), pf2: MUL(b, c, bc), pf3: MUL(ab, c, abc)) : MUL(a, bc, abc) =
    case+ pf1 of
        | MULbas()     => MULbas()
        | MULind(pf1') =>
            case+ pf2 of
                | MULbas()     => mul_nx0_0 {a} ()
                | MULind(pf2') =>
                    case+ pf3 of
                        | MULbas()     =>
                            sif a == 0
                            then MULbas()
                            else mul_nx0_0 {a} ()
                        | MULind(pf3') => MULind(mul_assoc1(pf1', pf2', pf3'))
in
    sif a < 0
    then let
        prval _pf1 = mul_neg_1(pf1)
        prval _pf3 = mul_neg_1(pf3)
    in
        sif b < 0
        then let
            prval __pf1 = mul_neg_2(_pf1)
            prval _pf2  = mul_neg_1(pf2)
            prval __pf3 = mul_neg_1(_pf3)
        in
            sif c < 0
            then let
                prval __pf2  = mul_neg_2(_pf2)
                prval ___pf3 = mul_neg_2(__pf3)
            in
                MULneg(mul_assoc1(__pf1, __pf2, ___pf3))
            end
            else MULneg(mul_neg_2(mul_assoc1(__pf1, _pf2, __pf3)))
        end
        else MULneg(mul_assoc1(_pf1, pf2, _pf3))
    end
    else sif b < 0
        then sif c < 0
            then let
                    prval _pf1 = mul_neg_2(pf1)
                    prval _pf2 = mul_neg_1(mul_neg_2(pf2))
                    prval _pf3 = mul_neg_1(mul_neg_2(pf3))
                in
                    mul_assoc1(_pf1, _pf2, _pf3)
                end
            else let
                    prval _pf1 = mul_neg_2(pf1)
                    prval _pf2 = mul_neg_2(pf2)
                    prval _pf3 = mul_neg_2(pf3)
                in
                    MULneg(mul_assoc1(_pf1, _pf2, _pf3))
                end
        else sif c < 0
            then let
                    prval _pf2 = mul_neg_1(pf2)
                    prval _pf3 = mul_neg_1(pf3)
                in
                    MULneg(mul_assoc1(pf1, _pf2, _pf3))
                end
            else mul_assoc1(pf1, pf2, pf3)
end

implement main0 () = ()

Мотивация кода - выполнить простое упражнение с использованием системы зависимых типов: доказать, что умножение целых чисел ассоциативно. Идея доказательства состоит в том, чтобы разбить 3 целочисленных переменных, a, b, c, на возможные случаи для их знаков, а затем свести задачу к доказательству ассоциативности для умножения натуральных чисел, где мы можем использовать индукцию.

Математически, эта стратегия должна быть разумной (хотя разбивать дела и принимать огромное дерево решений было утомительно). Проблема в том, что, когда я пытаюсь скомпилировать указанный выше файл с помощью команды patscc assoc.dats, я получаю следующее сообщение об ошибке:

assoc.dats: 591(line=20, offs=27) -- 599(line=20, offs=35): error(3): unsolved constraint: C3NSTRprop(C3TKmain(); S2Eeqeq(S2Eintinf(0); S2Evar(abc(4303))))
typechecking has failed: there are some unsolved constraints: please inspect the above reported error message(s) for information.
exit(ATS): uncaught exception: _2tmp_2ATS_2dPostiats_2src_2pats_error_2esats__FatalErrorExn(1025)

Честно говоря, я понятия не имею, как интерпретировать это сообщение об ошибке. Что такое ограничение C3NSTRprop(C3TKmain(); S2Eeqeq(S2Eintinf(0); S2Evar(abc(4303))))?

Answer 1

Есть несколько проблем с текущим кодом. Например, следующий случай не работает:

   case+ pf1 of
        | MULbas()     => MULbas()

, потому что abc == 0 еще не доказано. Это можно легко исправить следующим образом:

   case+ pf1 of
        | MULbas()     => let prval MULbas() = pf3 in MULbas() end       

Я бы не советовал продолжать с текущим кодом доказательства.

В общем, если вы хотите доказать теоремы, касающиеся MUL, из первого принципа, тогда вам почти всегда нужны следующие две проверочные функции:

extern
prfun
mul_is_tot
{a,b:int}() : [c:int] MUL(a, b, c)

extern
prfun
mul_is_fun
{a,b,c1,c2:int}
( pf1: MUL(a, b, c1)
, pf2: MUL(a, b, c2)): [c1==c2] void

Кстати, следующая реализация mul_assoc проходит проверку типов:

extern
prfun
mul_is_tot
{a,b:int}() : [c:int] MUL(a, b, c)

extern
prfun
mul_is_fun
{a,b,c1,c2:int}
( pf1: MUL(a, b, c1)
, pf2: MUL(a, b, c2)): [c1==c2] void

extern
prfun
mul_distrib
{a,b,c,ac,bc:int}
( MUL(a, c, ac)
, MUL(b, c, bc)): MUL(a+b, c, ac+bc)

extern
prfun
mul_assoc
{a,b,c,ab,bc,abc:int}
( pf1: MUL(a, b, ab),
  pf2: MUL(b, c, bc),
  pf3: MUL(ab, c, abc)): MUL(a, bc, abc)

extern
prfun
mul_neg_1
{m,n,p:int}(MUL(m, n, p)): MUL(~m, n, ~p)

primplmnt
mul_assoc
{a,b,c
,ab,bc,abc:int}
(pf1, pf2, pf3) =
(
sif
(a >= 0)
then
mul_assoc1(pf1, pf2, pf3)
else
mul_neg_1(mul_assoc1(mul_neg_1(pf1), pf2, mul_neg_1(pf3)))
) where
{
prfun
mul_assoc1
{a:nat
;b,c,ab,bc,abc:int} .<a>.
( pf1: MUL(a, b, ab),
  pf2: MUL(b, c, bc),
  pf3: MUL(ab, c, abc)): MUL(a, bc, abc) =
(
case+ pf1 of
| MULbas() =>
  let
  prval MULbas() = pf3 in MULbas()
  end
| MULind(pf1') => // a = a'+1 // ab = a'b + b                                                                                                                                                                                                                                 
  let
  prval pf3' = mul_is_tot() // (a'*b)*c                                                                                                                                                                                                                                       
  prval res' = mul_assoc1(pf1', pf2, pf3') // (a'*b)*c = a'*(b*c)                                                                                                                                                                                                             
  prval (  ) = mul_is_fun(pf3, mul_distrib(pf3', pf2))
  in
    MULind(res')
  end
)
} (* end of [mul_assoc] *)

Answer 2

Ограничение говорит о том, что средство проверки типов не может доказать, что статическая переменная abc (со штампом 4303) равна 0. S2E - это префикс, который означает статическое выражение на уровне 2 (среди нескольких уровней перевода.)

Исходя из номера строки сообщения, вам, вероятно, потребуется что-то вроде MULprop_m_0_p_0 из https://www.cs.bu.edu/~hwxi/ATS/TUTORIAL/contents/dataprops.dats.