Как ядро работает в теореме LCF Prover

Question

Я слышал, что в прорезателях теорема на основе LCF на основе LCF представляет собой некоторые функции для создания значений теоремы типа.Я верю, что они основаны на абстрактных типах данных.

Может ли кто-нибудь набросать псевдо-код Как эта работа?(В случае правильности вышеуказанного)

Answer 1

Вот несколько мыслей и код из ядра (файл thm.ml в isabelle / pure) от isabelle:

abstype thm = Thm of
 deriv *                        (*derivation*)
 {cert: Context.certificate,    (*background theory certificate*)
  tags: Properties.T,           (*additional annotations/comments*)
  maxidx: int,                  (*maximum index of any Var or TVar*)
  shyps: sort Ord_List.T,       (*sort hypotheses*)
  hyps: term Ord_List.T,        (*hypotheses*)
  tpairs: (term * term) list,   (*flex-flex pairs*)
  prop: term}                   (*conclusion*)
and deriv = Deriv of
 {promises: (serial * thm future) Ord_List.T,
  body: Proofterm.proof_body}
with

.

Также вот цитата из книги Полсона на мл. О абстрактных данных, которые он говорит:

Модульная структура облегчает понять программу. Лучше еще, Модули должны служить взаимозаменяемыми частями: замена одного модуля по Улучшенная версия не должна требовать изменения остальных. программа. Стандартный Абстрактные типы ML и функторы могут помочь нам также удовлетворить эту цель. Модуль может раскрыть его внутренние детали. Когда модуль заменяется, другой Части программы, которые зависят от таких деталей, потерпят неудачу. ML обеспечивает несколько способы объявления абстрактного типа и связанных с ними операций, скрываясь в типе представление.

Таким образом, вы не можете создать экземпляр абстрактного DataType, вы можете использовать его (его поля + функции). Дело о том, как вы реализуете эту функцию, очень зависит от языка. Если вы хотите сделать это в лямбда-исчислении, должно быть что-то подобное в книге Tapl Benjamin Pierce, на более поздних главах.

Приятная ссылка на это также Здесь .

Answer 2

Если я помню правильно, это была глава 5 или 6 из Джона Харрисона Справочника практической логики и автоматизированные рассуждения .

Джон Стерлинг написал некоторые Notes Для чтения в год или два назад, специально для LCF Prover, используя последовательный исчислений.