Nuprl Definition : has-value

If ⌜a⌝ has value then the call-by-value term 
eval a; 0⌝ evaluates to 0. If ⌜a⌝ diverges then so does ⌜eval a; 0⌝.
Thus, ⌜a⌝ has value if and only if  ⌜0 ≤ eval a; 0⌝⋅

(a)↓ ==  0 ≤ eval a; 0

Definitions occuring in Statement :  callbyvalue: callbyvalue natural_number: $n sqle: s ≤ t
Definitions occuring in definition :  sqle: s ≤ t callbyvalue: callbyvalue natural_number: $n
Rules referencing :  divergentSqle divergentSqlen compactness callbyvalueApply callbyvalueApplyCases exceptionApplyCases sqleLambda callbyvalueCallbyvalue callbyvalueIspair callbyvalueIsaxiom callbyvalueIsinl callbyvalueIsinr callbyvalueIslambda callbyvalueIsint callbyvalueIsatom callbyvalueIsatom1 callbyvalueIsatom2 ispairExceptionCases isintExceptionCases isaxiomExceptionCases isatomExceptionCases isinlExceptionCases isinrExceptionCases islambdaExceptionCases isatom1ExceptionCases isatom2ExceptionCases applyExceptionCases callbyvalueExceptionCases bottomDivergent
FDL editor aliases :  has-value

(a)\mdownarrow{}  ==    0  \mleq{}  eval  a;  0

Date html generated: 2016_07_08-PM-04_46_56
Last ObjectModification: 2015_09_22-PM-05_44_34

Theory : call!by!value_1

Home Index