Лемма как тип в записи - PullRequest
Новая
       7

Лемма как тип в записи

0 голосов
/ 08 апреля 2019

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

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

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

1 Ответ

4 голосов
/ 09 апреля 2019

То, что вы пишете, не имеет смысла, поскольку обозначение _ ==> _ должно связывать два логических значения.Но 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 значения.Они представляют разные вещи, которые иногда могут быть объединены, но вам нужно прояснить это различие, чтобы оставить категорию новичка .

для вашего последнего предложения "что значит иметьквантифицированная лемма как тип "здесь является другим объяснением.

При программировании на обычном языке программирования вы можете возвращать массивы целых чисел.Тем не менее, вы не можете быть явным и сказать, что вы хотите вернуть массив целых чисел определенной длины .В 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.

...