deniok: (typed lambda)
У него там неонка дджин внутри. Тактика tauto доказывает пропозициональные тавтологии, монтируя лямбда-терм подходящего типа

Coq < Variables A B C : Prop.
A is assumed
B is assumed
C is assumed

Coq < Lemma he_he : (B -> C) -> (A -> B) -> A -> C.
1 subgoal

  A : Prop
  B : Prop
  C : Prop
  ============================
   (B -> C) -> (A -> B) -> A -> C

he_he < tauto.
Proof completed.

he_he < Qed.
 tauto.
he_he is defined

Coq < Print he_he.
he_he =
fun (H : B -> C) (H0 : A -> B) (H1 : A) =>
let H2 := H0 H1 in let H3 := H H2 in H3
     : (B -> C) -> (A -> B) -> A -> C
Здесь fun вместо лямбды и типизация связанных в лямбда-терме переменных явная, чёрчевская.

Но можно и примитивными тактиками intros; apply H; apply H0; assumption:Read more... )Всякому видно, что при ручной работе и терм-композитор выходит кратким и выразительным, не то что эти вложенные let'ы ;-)
deniok: (Default)
Продираюсь (с удовольствием) через "Theorems for Free!" Вадлера
http://citeseer.ist.psu.edu/wadler89theorems.html

и не встречаю там термина Curry-Howard изоморфизм. Ни разу. Хотя речь-то о нём. Или нет?

Profile

deniok: (Default)
deniok

April 2017

S M T W T F S
      1
23 45678
9101112131415
16171819202122
23242526272829
30      

Syndicate

RSS Atom

Most Popular Tags

Style Credit

Expand Cut Tags

No cut tags
Page generated Jul. 27th, 2017 02:25 am
Powered by Dreamwidth Studios