(only non hidden objects are presented)
COM | bar_primitives | The four basic primitives of the partial type library are: bar(T) the type containing elements of T and all divergent terms t in! T the assertion that t halts and t is in bar(T) T admissible the assertion that fixpoint induction may be performed over T T total the assertion that every element of T halts |
DISP | bar | bar( < T:type:* > )== bar( < T > ) |
DISP | halt | Parens ::Prec(atomrel)::Index 0 :: {[SOFT} < e:term:L > {\\ }in! {- > 0} < T:type:L > { < -}{]} == < e > in! < T > Parens ::Prec(postop):: < e:term:E > halts== < e > halts |
DISP | admiss | Parens ::Prec(postop):: < T:type:E > admissible== < T > admissible |
DISP | total | Parens ::Prec(postop):: < T:Type:E > total== < T > total |
COM | bar_com | We want to be able to form halting assertions t in! T whenever t is in bar(T). For this to be sound, T must not equate any convergent and divergent elements. We instead require the stronger condition that T contains only convergent elements. This seems to make things work out more nicely in practice. |
RULE | barEquality | H bar(A) = bar(B) BY barEquality () H A = B H A total |
RULE | barInclusion | H a = a' BY barInclusion level{i} H a = a' H bar(A) = bar(A) |
RULE | bar_memberEquality | H a = a' BY bar_memberEquality level{i} z B C H a in! B a' in! C H, z:a in! B a = a' H bar(A) |
COM | halt_com | We use a typed halting assertion t in! T rather than a simpler untyped halting condition for the following reason: For t in! T to be well-formed in a sequent, we need it to be functional over the hypotheses. With typed halting, we can simply require that t is in bar(T) and bar(T) is functional over the hypotheses. With untyped halting, we would have to show that t's halting behavior is functional over all the hypotheses, which would be impossible to ever prove. |
RULE | haltEquality | H (a in! A) = (b in! B) BY haltEquality () H a = b H bar(A) = bar(B) |
RULE | halt_axiomEquality | H, Ax = Ax BY halt_axiomEquality () H a in! A |
RULE | haltUniversal | H a in! A BY haltUniversal B H a in! B H a = a |
RULE | termination | H a = b BY termination () H a in! A H a = b |
RULE | member_termination | H a = a BY member_termination () H a in! A |
COM | bottom_com | Introducing special rules for bottom are just for convenience. It would have been possible to prove the existence of a divergent term (say, the fixpoint of the flip function), which by bar_memberEquality would have been divergent in every bar type. |
RULE | bottomEquality | H Y (x.x) = Y (x.x) BY bottomEquality level{i} H bar(A) = bar(A) |
RULE | bottomDivergent | H Void BY bottomDivergent x A H Y (x.x) in! A |
COM | total_com | Totality has to be primitive. If we tried to define it as T total iff x:bar(T). x in! T well-formedness would depend upon bar(T) being well-formed, which is only the case if T is total. This would make totality non-negatable. |
RULE | totalEquality | H, A total = B total BY totalEquality () H A = B |
RULE | total_axiomEquality | H, Ax = Ax BY total_axiomEquality () H A total |
RULE | totality | H a in! A BY totality () H A total H a = a |
COM | admiss_com | The admissibility assertion, T admissible, is true whenever fixpoint induction can be performed on T. |
RULE | admissEquality | H, A admissible = B admissible BY admissEquality () H A = B |
RULE | admiss_axiomEquality | H, Ax = Ax BY admiss_axiomEquality () H A admissible |
COM | fixpoint_com | This is the critical rule to the theory of partial types, but semantically speaking it says nothing, since admissibility means that fixpoint induction may be performed. So this is just the elimination form for admissibility. |
RULE | fixpoint_induction | H Y f = Y f BY fixpoint_induction () H f = f H A admissible |
COM | totality_com | Most types are total. In particular, unions, products and functions are total since the intro forms are canonical and halt computation. This specifies that this is a lazy computation system. In an eager system computation would continue within product and union intros at least. Set and quotient types are total when their underlying types are. |
RULE | voidTotal | H, Void total BY voidTotal () No Subgoals |
RULE | intTotal | H, total BY intTotal () No Subgoals |
RULE | atomTotal | H, Atom total BY atomTotal () No Subgoals |
RULE | equalityTotal | H, (a1 = a2) total BY equalityTotal level{i} H (a1 = a2) = (a1 = a2) |
RULE | unionTotal | H, (A + B) total BY unionTotal level{i} H A + B = A + B |
RULE | productTotal | H, (x:A B) total BY productTotal level{i} H x:A B = x:A B |
RULE | functionTotal | H, (x:A B) total BY functionTotal level{i} H x:A B = x:A B |
RULE | setTotal | H, {x:A| B} total BY setTotal level{i} H A total H {x:A| B} = {x:A| B} |
RULE | quotientTotal | H, x,y:A//B total BY quotientTotal level{i} H A total H x,y:A//B = x,y:A//B |
COM | admissibility_com | At present there are no rules showing admissibility for dependent products, sets or quotients, but we want some. The present situation is particularly unsatisfying since it makes it impossible to perform t he usual predicate fixpoint induction. |
RULE | intAdmissible | H, admissible BY intAdmissible () No Subgoals |
RULE | atomAdmissible | H, Atom admissible BY atomAdmissible () No Subgoals |
RULE | equalityAdmissible | H, (a1 = a2) admissible BY equalityAdmissible level{i} H (a1 = a2) = (a1 = a2) |
RULE | unionAdmissible | H, (A + B) admissible BY unionAdmissible () H A admissible H B admissible |
RULE | functionAdmissible | H, (x:A B) admissible BY functionAdmissible () H A admissible H, x:A B admissible |
RULE | prodAdmissible | H, (A B) admissible BY prodAdmissible () H A admissible H B admissible |
ML | bar_basic_tactics | loadt `~crary/kml/prl/bar-basic-tactics` ;; |
THM | total_wf | A:. A total |
THM | bar_wf | A:. A total bar(A) |
THM | halt_wf | A:. A total (a:bar(A). (a in! A) ) |
THM | admiss_wf | A:. A admissible |
DISP | bottom_df | Bot== Bot |
ABS | bottom | Bot == Y (x.x) |
THM | bottom_wf | A:. A total Bot bar(A) |
THM | bottom_diverge | A:. A total (Bot in! A) |
THM | nat_total | total |
COM | partial_term_com | For any strict n-place operator there will need to be n+2 partial term rules: 1) a rule for membership in the bar type op(t1, ..., tn) in bar(T) if for each i, ti in bar(Si) 2) a rule for halting op(t1, ..., tn) in! T if for each i, ti in! Si 3) n rules for inducement ti in! Si if op(t1, ..., tn) in! T None of these rules are derivable from the original typing rule op(t1, ..., tn) in T if for each i, ti in Si but the original typing rule is derivable from the halting rule and the totality and member_termination rules, so long as each Si is total. If op is nonstrict in position k, the kth subgoal of the halting rule would be dropped, as well as the kth inducement rule. At present, partial term rules are only in place for subtraction. They need to be put in for every operator. |
RULE | subtract_barEquality | H, m1 - n1 = m2 - n2 BY subtract_barEquality () H m1 = m2 H n1 = n2 |
RULE | subtractHalt | H (e1 - e2) halts BY subHalt () H e1 halts H e2 halts |
RULE | subtractInduceLeft | H e1 halts BY subInduceLeft e2 H (e1 - e2) halts H e1 = e1 |
RULE | subtractInduceRight | H e2 halts BY subInduceRight e1 H (e1 - e2) halts |
COM | seq_com | One more primitive operator is the sequencing operator: the term " t1; t2 " is equivalent to t2 if t1 halts. This allows us to embed eager progra mming systems in this one, and also is critical to deriving results in recur sion theory. |
DISP | seq | EdAlias seq ::Parens :: < e1:term:L > ; < e2:term:E > == < e1 > ; < e2 > |
RULE | seqEquality | H (e1; e2) = (e1'; e2') BY seqEquality B H e1 = e1' H e2 = e2' |
RULE | seqReduce | H (e1; e2) = e2 BY seqReduce B H e1 in! B H e2 = e2 |
RULE | seqHalt | H (e1; e2) in! A BY seqHalt B H e1 in! B H e2 in! A |
RULE | seqInduceLeft | H e1 in! A BY seqInduceLeft e2 B H (e1; e2) in! B H e1 = e1 |
RULE | seqInduceRight | H e2 in! A BY seqInduceRight e1 H (e1; e2) in! A |
ML | bar_tactics | loadt `~crary/kml/prl/bar-tactics` ;; |