Блог

Новичок здесь! Как нам интерпретировать запись, которая выглядит примерно так?

  Record test A B :=
{
  CA: forall m, A m; 
  CB: forall a b m, CA m ==> B(a,b);
}
  

Я пытаюсь получить представление о том, как будет выглядеть экземпляр этой записи и, более того, что значит иметь количественную лемму в качестве типа.

То, что вы пишете, не может иметь смысла, потому что обозначение _ ==> _ должно связывать два логических значения. Но CA имеет тип A m , который сам по себе является типом, а не логическим значением.

Одной из возможностей продвижения вперед было бы создание CA логической функции, которая могла бы представлять A предикат.

Еще одна трудность с вашей гипотетической записью заключается в том, что мы не знаем, каковы типы ввода для A и B , поэтому я предположу, что мы живем в окружающем типе, T над которым появляются количественные оценки. Итак, вот вариант:

 Record test (T : Type) (A : T -> Prop) (B : T * T -> bool) :=
{
  CA : T -> bool;
  CA_A : forall m, CA m = true -> A m;
  CB : forall a b m, (CA m ==> B(a, b)) = true
}.
  

Этот пример заставляет вас понять, что в этом логическом языке есть два разных понятия: bool значения и Prop values. Они представляют разные вещи, которые иногда могут быть объединены, но вам нужно четко провести различие в своей голове, чтобы выйти из категории начинающих.

Для вашего последнего предложения «что значит иметь количественную лемму как тип» вот еще одно объяснение.

При программировании на обычном языке программирования вы можете возвращать массивы целых чисел. Однако вы не можете быть явным и сказать, что хотите вернуть массив целых чисел определенной длины. В Gallina (базовом языке программирования Coq) вы можете определить тип массивов длиной 10. Давайте предположим, что такой тип был бы записан array n . Так что array 10 и array 11 были бы двумя разными типами. Функция, которая принимает в качестве входных данных число n и возвращает в качестве выходных данных массив длины n , будет иметь следующий тип:

forall n, array n

Таким образом, объект, который имеет количественную формулу в качестве типа, просто является функцией.

С логической точки зрения утверждение forall n, array n обычно читается как для каждого n существует массив size n . Это утверждение, вероятно, вас не удивляет.

Таким образом, тип массива зависит от индекса. Теперь мы можем подумать о другом типе, например, о типе доказательств, который n является простым. Давайте предположим, что этот тип записан prime n . Конечно, есть числа, которые не являются простыми, поэтому, например, тип prime 4 вообще не должен содержать никаких доказательств. Теперь я могу написать вызываемую функцию test_prime : nat -> bool со свойством, что, когда она возвращает true , у меня есть гарантия, что входные данные являются простыми. Это было бы записано как таковое:

 forall n, test_prime n = true -> prime n
  

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

 Record certified_prime_test :=
  {
     test_prime : nat -> bool;
     certificate : forall n, test_prime n = true -> prime nat
  }.
  

Таким образом, записи, содержащие универсальные количественные формулы, могут относиться к одной из этих двух категорий: либо один компонент является частью этой функции, выходные данные которой различаются для нескольких типов одного семейства (как в примере array ), либо один из компонентов фактически предоставляет больше логической информации о другом компоненте, который является функцией. В certified_prime_test примере certificate компонент предоставляет больше информации о test_prime функции.