Что означает определение функции Coq `Определение Термин: = forall T: Тип, термин T`? - PullRequest
Новая
       16

Что означает определение функции Coq `Определение Термин: = forall T: Тип, термин T`?

0 голосов
/ 25 июня 2018

Я читаю о механизации линейной логики в Coq http://www.cs.cmu.edu/~iliano/projects/metaCLF2/inc/dl/papers/lsfa17.pdf и https://github.com/brunofx86/LL, и у меня возникают проблемы с пониманием определения функции Term (и других определений функций, включающих forall) из https://github.com/brunofx86/LL/blob/master/FOLL/LL/SyntaxLL.v:

Definition Term := forall T:Type,  term T. (* type for terms *)
Definition AProp := forall T:Type, aprop T. (* type for atomic propositions *)

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

Я читаю http://adam.chlipala.net/cpdt/cpdt.pdf '' Глава 12 Юниверсы и Аксиомы '', этот вопрос является продолжением моего предыдущего вопроса Как понять конструктор типа Coq var (t: T) , пытаясь понять эту упомянутую статью.

1 Ответ

0 голосов
/ 25 июня 2018

В параметрическом HOAS параметр T представляет набор переменных, которые могут встречаться в терме. Например, если вы хотите использовать термин, который использует не более двух переменных, он может иметь тип term bool, поскольку bool имеет двух жителей. Таким образом, закрытый член (без свободной переменной) может быть наивно набран term void, где void - пустой тип: 

Inductive void := .

term void оказывается эквивалентным forall A, term A (вы можете применить функцию forall A, void -> A в одном направлении и просто специализироваться в другом направлении). Последнее представление закрытых терминов удобнее встраивать в другие открытые термины.

...