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 coinductive relation 
on terms that says (essentially) that for any canonical form X, 
if computes to ⌜X[a1; a2; ...]⌝ 
then there exist terms b1, b2,... such that 
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 "contexual congruence relation".

It is an invariant of the Nuprl type system that all types are closed under
t⌝This justifies the rules for sqequal substitution


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

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