13208
|
1 |
(* Title: HOL/Prolog/Type.thy
|
|
2 |
Author: David von Oheimb (based on a lecture on Lambda Prolog by Nadathur)
|
|
3 |
*)
|
9015
|
4 |
|
63167
|
5 |
section \<open>Type inference\<close>
|
9015
|
6 |
|
17311
|
7 |
theory Type
|
|
8 |
imports Func
|
|
9 |
begin
|
9015
|
10 |
|
17311
|
11 |
typedecl ty
|
9015
|
12 |
|
51311
|
13 |
axiomatization
|
|
14 |
bool :: ty and
|
|
15 |
nat :: ty and
|
|
16 |
arrow :: "ty => ty => ty" (infixr "->" 20) and
|
|
17 |
typeof :: "[tm, ty] => bool" and
|
17311
|
18 |
anyterm :: tm
|
51311
|
19 |
where common_typeof: "
|
9015
|
20 |
typeof (app M N) B :- typeof M (A -> B) & typeof N A..
|
|
21 |
|
|
22 |
typeof (cond C L R) A :- typeof C bool & typeof L A & typeof R A..
|
|
23 |
typeof (fix F) A :- (!x. typeof x A => typeof (F x) A)..
|
|
24 |
|
|
25 |
typeof true bool..
|
|
26 |
typeof false bool..
|
|
27 |
typeof (M and N) bool :- typeof M bool & typeof N bool..
|
|
28 |
|
|
29 |
typeof (M eq N) bool :- typeof M T & typeof N T ..
|
|
30 |
|
|
31 |
typeof Z nat..
|
|
32 |
typeof (S N) nat :- typeof N nat..
|
|
33 |
typeof (M + N) nat :- typeof M nat & typeof N nat..
|
|
34 |
typeof (M - N) nat :- typeof M nat & typeof N nat..
|
|
35 |
typeof (M * N) nat :- typeof M nat & typeof N nat"
|
|
36 |
|
51311
|
37 |
axiomatization where good_typeof: "
|
9015
|
38 |
typeof (abs Bo) (A -> B) :- (!x. typeof x A => typeof (Bo x) B)"
|
|
39 |
|
51311
|
40 |
axiomatization where bad1_typeof: "
|
9015
|
41 |
typeof (abs Bo) (A -> B) :- (typeof varterm A => typeof (Bo varterm) B)"
|
|
42 |
|
51311
|
43 |
axiomatization where bad2_typeof: "
|
9015
|
44 |
typeof (abs Bo) (A -> B) :- (typeof anyterm A => typeof (Bo anyterm) B)"
|
|
45 |
|
21425
|
46 |
|
|
47 |
lemmas prog_Type = prog_Func good_typeof common_typeof
|
|
48 |
|
61337
|
49 |
schematic_goal "typeof (abs(%n. abs(%m. abs(%p. p and (n eq m))))) ?T"
|
21425
|
50 |
apply (prolog prog_Type)
|
|
51 |
done
|
|
52 |
|
61337
|
53 |
schematic_goal "typeof (fix (%x. x)) ?T"
|
21425
|
54 |
apply (prolog prog_Type)
|
|
55 |
done
|
|
56 |
|
61337
|
57 |
schematic_goal "typeof (fix (%fact. abs(%n. (app fact (n - Z))))) ?T"
|
21425
|
58 |
apply (prolog prog_Type)
|
|
59 |
done
|
|
60 |
|
61337
|
61 |
schematic_goal "typeof (fix (%fact. abs(%n. cond (n eq Z) (S Z)
|
21425
|
62 |
(n * (app fact (n - (S Z))))))) ?T"
|
|
63 |
apply (prolog prog_Type)
|
|
64 |
done
|
|
65 |
|
61337
|
66 |
schematic_goal "typeof (abs(%v. Z)) ?T" (*correct only solution (?A1 -> nat) *)
|
21425
|
67 |
apply (prolog prog_Type)
|
|
68 |
done
|
|
69 |
|
61337
|
70 |
schematic_goal "typeof (abs(%v. Z)) ?T"
|
21425
|
71 |
apply (prolog bad1_typeof common_typeof) (* 1st result ok*)
|
|
72 |
done
|
|
73 |
|
61337
|
74 |
schematic_goal "typeof (abs(%v. Z)) ?T"
|
21425
|
75 |
apply (prolog bad1_typeof common_typeof)
|
|
76 |
back (* 2nd result (?A1 -> ?A1) wrong *)
|
|
77 |
done
|
|
78 |
|
61337
|
79 |
schematic_goal "typeof (abs(%v. abs(%v. app v v))) ?T"
|
21425
|
80 |
apply (prolog prog_Type)? (*correctly fails*)
|
|
81 |
oops
|
|
82 |
|
61337
|
83 |
schematic_goal "typeof (abs(%v. abs(%v. app v v))) ?T"
|
21425
|
84 |
apply (prolog bad2_typeof common_typeof) (* wrong result ((?A3 -> ?B3) -> ?A3 -> ?B3)*)
|
|
85 |
done
|
17311
|
86 |
|
9015
|
87 |
end
|