Карри-Говард для синтеза терминов в Изабель - PullRequest
Новая
       74

Карри-Говард для синтеза терминов в Изабель

0 голосов
/ 15 ноября 2018

Скажем, я доказал некоторые основные положения интуиционистской логики высказываний в Изабель / HOL: 

theorem ‹(A ⟶ B) ⟶ ((B ⟶ C) ⟶ (A ⟶ C))›
proof -
  {
    assume ‹A ⟶ B›
    {
      assume ‹B ⟶ C›
      {
        assume ‹A›
        with ‹A ⟶ B› have ‹B› by (rule mp)
        with ‹B ⟶ C› have ‹C› by (rule mp)
      }
      hence ‹A ⟶ C› by (rule impI)
    }
    hence ‹(B ⟶ C) ⟶ (A ⟶ C)› by (rule impI)
  }
  thus ?thesis by (rule impI)
qed

Я знаю из соответствия Карри-Говарда, что это предложение соответствует некоторому типу (a -> b) -> ((b -> c) -> (a -> c)), и доказательстводо некоторого термина, все внутри некоторой теории типов (скажем, в простонизированном λ-исчислении).Из структуры доказательства я знаю, что соответствующий просто набранный λ-член равен λf:a→b. λg:b→c. λx:a. f(g(x)).

Есть ли способ заставить Изабель сконструировать это для меня?

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

Я также знаю, что HOL - это не то же самое, что теория зависимого типа, которая, как я понимаю, имеет более сильный аромат Карри-Ховарда.Я знаю, что сам HOL концептуально в некотором роде похож на полиморфное λ-исчисление, и я нашел несколько кратких заметок о том, как HOL является поверхностным кодированием логики в теории типов, но будет весьма полезен некоторый дополнительный контекст.Я едва смог собрать воедино, как все эти разные помощники по доказательству и связанные с ними основы связаны друг с другом, и, возможно, какой-то более исторический контекст также поможет.К сожалению, документация вокруг Изабель, Кок и т. Д. Кажется немного повсеместной;в частности, для Изабель я, кажется, регулярно нахожу информацию, которая устарела на 20 лет.

...