Nuprl Definition : sqle def
This is Doug Howe's computational simulation relation on terms.
We call if "squiggle" less-or-equal or `sqle`.
The simulation ⌜s ≤ t⌝ is a coinductive relation
on terms that says (essentially) that for any canonical form X,
if s computes to ⌜X[a1; a2; ...]⌝
then there exist terms b1, b2,... such that
t computes to ⌜X[b1; b2; ...]⌝
and ⌜a1 ≤ b1⌝,⌜a2 ≤ b2⌝,...
See also the documentation for ⌜s ~ t⌝.⋅
s ≤ t == PRIMITIVE
Rules referencing :
exceptionNotBottom,
exceptionNotAxiom,
divergentSqle,
axiomSqleEquality,
sqequalSqle,
sqleDefinition,
sqleReflexivity,
sqleTransitivity,
sqleRule,
sqleExtensionalEquality,
sqleIntensionalEquality,
fixpointLeast,
callbyvalueReduce,
callbyvalueInt,
callbyvalueAtom1,
callbyvalueAtom2,
callbyvalueAtom,
callbyvalueType,
callbyvalueAdd,
callbyvalueMultiply,
callbyvalueDivide,
callbyvalueRemainder,
callbyvalueMinus,
callbyvalueLess,
callbyvalueIntEq,
callbyvalueAtomEq,
callbyvalueAtomnEq,
callbyvalueApply,
callbyvalueApplyCases,
exceptionApplyCases,
tryReduceValue,
sqleLambda,
applyPair,
applyInl,
applyInr,
applyInt,
callbyvalueCallbyvalue,
callbyvalueSpread,
callbyvalueDecide,
callbyvalueIspair,
callbyvalueIsaxiom,
callbyvalueIsinl,
callbyvalueIsinr,
callbyvalueIslambda,
callbyvalueIsint,
callbyvalueIsatom,
callbyvalueIsatom1,
callbyvalueIsatom2,
ispairCases,
isintCases,
isatomCases,
isaxiomCases,
islambdaCases,
isinlCases,
isinrCases,
isatom1Cases,
isatom2Cases
Latex:
s \mleq{} t == PRIMITIVE
Date html generated:
2016_07_08-PM-04_46_23
Last ObjectModification:
2015_10_30-AM-11_52_45
Theory : core_1
Home
Index