/
typeinh.pro
71 lines (57 loc) · 1.98 KB
/
typeinh.pro
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
:- set_prolog_flag(occurs_check, true).
:- op(160, fx, ⊢).
:- op(150, xfx, ⊢).
:- op(145, xfx, @≡).
:- op(140, xfx, #).
:- op(140, xfx, :).
:- op(120, xfy, ⇒).
:- op(100, yfx, @).
/*
Термове
1. x
2. M @ N
3. λ(x, N)
Типове
1. α
2. Ρ ⇒ Σ
Типови съждения
M : Τ.
Списъци
1. []
2. [X | T]
Контекст = списък от типови съждения (с условие)
Γ ⊢ M : Τ.
*/
i(λ(x, x)).
k(λ(x, λ(y, x))).
kstar(λ(x, λ(y, y))).
s(λ(x, λ(y, λ(z, x@z@(y@z))))).
omega(λ(x, x@x)).
ti(α ⇒ α).
tk(α ⇒ β ⇒ α).
ts((α ⇒ β ⇒ γ) ⇒ (α ⇒ β) ⇒ α ⇒ γ).
ty((α ⇒ α) ⇒ α).
tc(α ⇒ (α ⇒ β) ⇒ β).
tz((β ⇒ α) ⇒ (α ⇒ β) ⇒ β).
% +Γ ⊢ -M : +T
% Γ#V ↔ Контекст Γ и стек от типове V
⊢ M : Τ :- []#[] ⊢ M : Τ.
Γ#_ ⊢ X : Τ :- member(X : Τ, Γ).
Γ#V ⊢ λ(X, N) : Ρ ⇒ Σ :- [ X : Ρ | Γ ]#V ⊢ N : Σ.
Γ#V ⊢ M : Τ :- not(member(Τ, V)),
member(X : Ρ, Γ), Γ#[Τ|V] ⊢ X : Ρ @≡ M : Τ.
/* В Γ имаме декларация от вида X : Σ₁ ⇒ Σ₂ ⇒ ... ⇒ Σₖ ⇒ Τ
и освен това можем да намерим термове
N₁, ...., Nₖ, така че Γ ⊢ Nᵢ : Σᵢ
тогава полагаме M := X@N₁...@Nₖ
*/
/*
Γ ⊢ Q : Ρ @≡ M : Τ
↔
Съществуват типове Σ₁, ..., Σₖ ,така че Σ₁ ⇒ Σ₂ ⇒ ... ⇒ Σₖ ⇒ Τ ≡ Ρ
Съществуват термове N₁, ...., Nₖ, така че Γ ⊢ Nᵢ : Σᵢ
и освен това Q@N₁...@Nₖ ≡ M
+Γ ⊢ +Q : +Ρ @≡ -M : +Τ
*/
_ ⊢ Q : Ρ @≡ Q : Ρ.
Γ#V ⊢ Q : Σ ⇒ Ρ @≡ M : Τ :- Γ#V ⊢ N : Σ, !, Γ#V ⊢ Q@N : Ρ @≡ M : Τ.