Nuprl Theory bar_1

(only non hidden objects are presented)

COMbar_primitivesThe 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
DISPbarbar( < T:type:* > )== bar( < T > )
DISPhaltParens ::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
DISPadmissParens ::Prec(postop):: < T:type:E > admissible== < T > admissible
DISPtotalParens ::Prec(postop):: < T:Type:E > total== < T > total
COMbar_comWe 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.
RULEbarEqualityH bar(A) = bar(B) BY barEquality () H A = B H A total
RULEbarInclusionH a = a' BY barInclusion level{i} H a = a' H bar(A) = bar(A)
RULEbar_memberEqualityH 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)
COMhalt_comWe 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.
RULEhaltEqualityH (a in! A) = (b in! B) BY haltEquality () H a = b H bar(A) = bar(B)
RULEhalt_axiomEqualityH, Ax = Ax BY halt_axiomEquality () H a in! A
RULEhaltUniversalH a in! A BY haltUniversal B H a in! B H a = a
RULEterminationH a = b BY termination () H a in! A H a = b
RULEmember_terminationH a = a BY member_termination () H a in! A
COMbottom_comIntroducing 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.
RULEbottomEqualityH Y (x.x) = Y (x.x) BY bottomEquality level{i} H bar(A) = bar(A)
RULEbottomDivergentH Void BY bottomDivergent x A H Y (x.x) in! A
COMtotal_comTotality 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.
RULEtotalEqualityH, A total = B total BY totalEquality () H A = B
RULEtotal_axiomEqualityH, Ax = Ax BY total_axiomEquality () H A total
RULEtotalityH a in! A BY totality () H A total H a = a
COMadmiss_comThe admissibility assertion, T admissible, is true whenever fixpoint induction can be performed on T.
RULEadmissEqualityH, A admissible = B admissible BY admissEquality () H A = B
RULEadmiss_axiomEqualityH, Ax = Ax BY admiss_axiomEquality () H A admissible
COMfixpoint_comThis 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.
RULEfixpoint_inductionH Y f = Y f BY fixpoint_induction () H f = f H A admissible
COMtotality_comMost 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.
RULEvoidTotalH, Void total BY voidTotal () No Subgoals
RULEintTotalH, total BY intTotal () No Subgoals
RULEatomTotalH, Atom total BY atomTotal () No Subgoals
RULEequalityTotalH, (a1 = a2) total BY equalityTotal level{i} H (a1 = a2) = (a1 = a2)
RULEunionTotalH, (A + B) total BY unionTotal level{i} H A + B = A + B
RULEproductTotalH, (x:A B) total BY productTotal level{i} H x:A B = x:A B
RULEfunctionTotalH, (x:A B) total BY functionTotal level{i} H x:A B = x:A B
RULEsetTotalH, {x:A| B} total BY setTotal level{i} H A total H {x:A| B} = {x:A| B}
RULEquotientTotalH, x,y:A//B total BY quotientTotal level{i} H A total H x,y:A//B = x,y:A//B
COMadmissibility_comAt 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.
RULEintAdmissibleH, admissible BY intAdmissible () No Subgoals
RULEatomAdmissibleH, Atom admissible BY atomAdmissible () No Subgoals
RULEequalityAdmissibleH, (a1 = a2) admissible BY equalityAdmissible level{i} H (a1 = a2) = (a1 = a2)
RULEunionAdmissibleH, (A + B) admissible BY unionAdmissible () H A admissible H B admissible
RULEfunctionAdmissibleH, (x:A B) admissible BY functionAdmissible () H A admissible H, x:A B admissible
RULEprodAdmissibleH, (A B) admissible BY prodAdmissible () H A admissible H B admissible
MLbar_basic_tacticsloadt `~crary/kml/prl/bar-basic-tactics` ;;
THMtotal_wfA:. A total
THMbar_wfA:. A total bar(A)
THMhalt_wfA:. A total (a:bar(A). (a in! A) )
THMadmiss_wfA:. A admissible
DISPbottom_dfBot== Bot
ABSbottomBot == Y (x.x)
THMbottom_wfA:. A total Bot bar(A)
THMbottom_divergeA:. A total (Bot in! A)
THMnat_total total
COMpartial_term_comFor 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.
RULEsubtract_barEqualityH, m1 - n1 = m2 - n2 BY subtract_barEquality () H m1 = m2 H n1 = n2
RULEsubtractHaltH (e1 - e2) halts BY subHalt () H e1 halts H e2 halts
RULEsubtractInduceLeftH e1 halts BY subInduceLeft e2 H (e1 - e2) halts H e1 = e1
RULEsubtractInduceRightH e2 halts BY subInduceRight e1 H (e1 - e2) halts
COMseq_comOne 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.
DISPseqEdAlias seq ::Parens :: < e1:term:L > ; < e2:term:E > == < e1 > ; < e2 >
RULEseqEqualityH (e1; e2) = (e1'; e2') BY seqEquality B H e1 = e1' H e2 = e2'
RULEseqReduceH (e1; e2) = e2 BY seqReduce B H e1 in! B H e2 = e2
RULEseqHaltH (e1; e2) in! A BY seqHalt B H e1 in! B H e2 in! A
RULEseqInduceLeftH e1 in! A BY seqInduceLeft e2 B H (e1; e2) in! B H e1 = e1
RULEseqInduceRightH e2 in! A BY seqInduceRight e1 H (e1; e2) in! A
MLbar_tacticsloadt `~crary/kml/prl/bar-tactics` ;;

the other theories