Nuprl Definition : sqequal def
This is Doug Howe's computational bi-simulation relation on terms.
We call if "squiggle" equality or `sqequal`.
It is equivalent to the conjunction of the comutational simulation
relations ⌜s ≤ t⌝ and ⌜t ≤ s⌝. (see: sqequalSqle)
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⌝,...
Using "Howe's trick" this relation is extended to open terms
(i.e. terms with free variables)
and proved to be a "contexual congruence relation".
It is an invariant of the Nuprl type system that all types are closed under
⌜s ~ t⌝. This justifies the rules for sqequal substitution
sqequalSubstitution
sqequalHypSubstitution
⋅
s ~ t == PRIMITIVE
Rules referencing :
computationStep,
computeAll,
isintReduceTrue,
isatomReduceTrue,
isAtom2ReduceTrue,
isAtom1ReduceTrue,
isintReduceAtom,
sqequalAxiom,
sqequalElimination,
sqequalDefinition,
sqequalSqle,
sqequalReflexivity,
sqequalTransitivity,
sqequalBase,
sqequalSubstitution,
sqequalHypSubstitution,
sqequalRule,
sqequalExtensionalEquality,
sqequalIntensionalEquality,
int_eqReduceTrueSq,
int_eqReduceFalseSq,
atomn_eqReduceTrueSq,
atom_eqReduceTrueSq,
atomn_eqReduceFalseSq,
atom_eqReduceFalseSq,
callbyvalueReduce,
callbyvalueApplyCases,
exceptionApplyCases,
tryReduceValue,
sqleLambda,
exceptionSqequal,
exceptionLess,
exceptionInteq,
exceptionAtomeq,
exceptionAtomeq1,
exceptionAtomeq2,
exceptionAdd,
exceptionMultiply,
exceptionDivide,
exceptionRemainder,
ispairCases,
isintCases,
isatomCases,
isaxiomCases,
islambdaCases,
isinlCases,
isinrCases,
isatom1Cases,
isatom2Cases,
lessCases
FDL editor aliases :
sim
Latex:
s \msim{} t == PRIMITIVE
Date html generated:
2016_07_08-PM-04_46_22
Last ObjectModification:
2015_10_30-AM-11_34_31
Theory : core_1
Home
Index