44 typeof (abs Bo) (A -> B) :- (typeof anyterm A => typeof (Bo anyterm) B)" |
44 typeof (abs Bo) (A -> B) :- (typeof anyterm A => typeof (Bo anyterm) B)" |
45 |
45 |
46 |
46 |
47 lemmas prog_Type = prog_Func good_typeof common_typeof |
47 lemmas prog_Type = prog_Func good_typeof common_typeof |
48 |
48 |
49 schematic_lemma "typeof (abs(%n. abs(%m. abs(%p. p and (n eq m))))) ?T" |
49 schematic_goal "typeof (abs(%n. abs(%m. abs(%p. p and (n eq m))))) ?T" |
50 apply (prolog prog_Type) |
50 apply (prolog prog_Type) |
51 done |
51 done |
52 |
52 |
53 schematic_lemma "typeof (fix (%x. x)) ?T" |
53 schematic_goal "typeof (fix (%x. x)) ?T" |
54 apply (prolog prog_Type) |
54 apply (prolog prog_Type) |
55 done |
55 done |
56 |
56 |
57 schematic_lemma "typeof (fix (%fact. abs(%n. (app fact (n - Z))))) ?T" |
57 schematic_goal "typeof (fix (%fact. abs(%n. (app fact (n - Z))))) ?T" |
58 apply (prolog prog_Type) |
58 apply (prolog prog_Type) |
59 done |
59 done |
60 |
60 |
61 schematic_lemma "typeof (fix (%fact. abs(%n. cond (n eq Z) (S Z) |
61 schematic_goal "typeof (fix (%fact. abs(%n. cond (n eq Z) (S Z) |
62 (n * (app fact (n - (S Z))))))) ?T" |
62 (n * (app fact (n - (S Z))))))) ?T" |
63 apply (prolog prog_Type) |
63 apply (prolog prog_Type) |
64 done |
64 done |
65 |
65 |
66 schematic_lemma "typeof (abs(%v. Z)) ?T" (*correct only solution (?A1 -> nat) *) |
66 schematic_goal "typeof (abs(%v. Z)) ?T" (*correct only solution (?A1 -> nat) *) |
67 apply (prolog prog_Type) |
67 apply (prolog prog_Type) |
68 done |
68 done |
69 |
69 |
70 schematic_lemma "typeof (abs(%v. Z)) ?T" |
70 schematic_goal "typeof (abs(%v. Z)) ?T" |
71 apply (prolog bad1_typeof common_typeof) (* 1st result ok*) |
71 apply (prolog bad1_typeof common_typeof) (* 1st result ok*) |
72 done |
72 done |
73 |
73 |
74 schematic_lemma "typeof (abs(%v. Z)) ?T" |
74 schematic_goal "typeof (abs(%v. Z)) ?T" |
75 apply (prolog bad1_typeof common_typeof) |
75 apply (prolog bad1_typeof common_typeof) |
76 back (* 2nd result (?A1 -> ?A1) wrong *) |
76 back (* 2nd result (?A1 -> ?A1) wrong *) |
77 done |
77 done |
78 |
78 |
79 schematic_lemma "typeof (abs(%v. abs(%v. app v v))) ?T" |
79 schematic_goal "typeof (abs(%v. abs(%v. app v v))) ?T" |
80 apply (prolog prog_Type)? (*correctly fails*) |
80 apply (prolog prog_Type)? (*correctly fails*) |
81 oops |
81 oops |
82 |
82 |
83 schematic_lemma "typeof (abs(%v. abs(%v. app v v))) ?T" |
83 schematic_goal "typeof (abs(%v. abs(%v. app v v))) ?T" |
84 apply (prolog bad2_typeof common_typeof) (* wrong result ((?A3 -> ?B3) -> ?A3 -> ?B3)*) |
84 apply (prolog bad2_typeof common_typeof) (* wrong result ((?A3 -> ?B3) -> ?A3 -> ?B3)*) |
85 done |
85 done |
86 |
86 |
87 end |
87 end |