Nuprl Definition : is-exception

Howe's `sqle` relation is enough to define the proposition
(about t ∈ Base) that is an exception.
Note that this is not decidable proposition! 
If being an exception were decidable, then program could 
catch *all* exceptions and we would not be able
to use exceptions to find the modulus of continuity of functionals.

The test ⌜isaxiom(e?n:x.Ax) ∧b isint(e?n:x.2)⌝ can be used to distinguish between
canonical values that are not exceptions and exceptions *with name n*.
But on other exceptions e', this test will raise the exception e'
(as it must, for our construction of the modulus of continuity to work.)

is-exception(t) ==  exception(⊥; ⊥) ≤ t

Definitions occuring in Statement :  sqle: s ≤ t
Definitions occuring in definition :  sqle: s ≤ t
Rules referencing :  divergentSqle divergentSqlen exceptionSqequal ispairExceptionCases isintExceptionCases isaxiomExceptionCases isatomExceptionCases isinlExceptionCases isinrExceptionCases islambdaExceptionCases isatom1ExceptionCases isatom2ExceptionCases decideExceptionCases spreadExceptionCases minusExceptionCases applyExceptionCases int_eqExceptionCases lessExceptionCases atom_eqExceptionCases atom1_eqExceptionCases atom2_eqExceptionCases addExceptionCases divideExceptionCases remainderExceptionCases multiplyExceptionCases callbyvalueExceptionCases
FDL editor aliases :  is-exception

is-exception(t)  ==    exception(\mbot{};  \mbot{})  \mleq{}  t

Date html generated: 2016_07_08-PM-04_46_54
Last ObjectModification: 2015_09_22-PM-05_44_33

Theory : call!by!value_1

Home Index