Неявные функции: карри и тотальность

Question

При указании неявной функции в VDM-SL возможно ли указать карри функцию? В следующих тестах test1 и test2 - явные функции без кеширования и с карри, а test3 - неявная функция без кеширования. Все принимаются Увертюрой. test4 - это попытка неявной функции карри, но она отвергается Overture.

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

module moduleName
  exports all
  definitions
  functions

  test1 : nat * nat +> nat
  test1 (arg1,arg2) == arg1+arg2;

  test2 : nat -> nat +> nat
  test2 (arg1) (arg2) == arg1+arg2;

  test3 (arg1:nat,arg2:nat) res:nat
  post res = arg1+arg2;

  test4 (arg1:nat) (arg2:nat) res:nat
  post res = arg1+arg2;

end moduleName

Answer 1

Нет, я боюсь, что функции карри предоставляются только для явных определений функций. И нет никакого частичного / полного индикатора для неявных определений.

(Я просто спросил, почему у нас такая разница. Похоже, это связано с историей языка: английская школа производила неявные функции, но без каррирования, тогда как в датской школе были явные функции с каррингом. Они действительно должны быть гармонизированы - и ваш предполагаемый синтаксис, вероятно, будет результатом.)