Nuprl Definition : simple-swap-test
simple-swap-test(AModel;prog;i;j) ==
A-bind(AModel) (A-coerce(AModel) (A-fetch'(AModel) i))
(λin@i.(A-bind(AModel) (A-coerce(AModel) (A-fetch'(AModel) j))
(λin@j.(A-bind(AModel) prog
(λx.(A-bind(AModel) (A-coerce(AModel) (A-fetch'(AModel) i))
(λout@i.(A-bind(AModel) (A-coerce(AModel) (A-fetch'(AModel) j))
(λout@j.(A-return(AModel) ((out@i =z in@j) ∧b (out@j =z in@i))))))))))))
Definitions occuring in Statement :
A-coerce: A-coerce(AModel),
A-fetch': A-fetch'(AModel),
A-bind: A-bind(AModel),
A-return: A-return(AModel),
band: p ∧b q,
eq_int: (i =z j),
apply: f a,
lambda: λx.A[x]
Definitions occuring in definition :
A-bind: A-bind(AModel),
A-coerce: A-coerce(AModel),
A-fetch': A-fetch'(AModel),
lambda: λx.A[x],
apply: f a,
A-return: A-return(AModel),
band: p ∧b q,
eq_int: (i =z j)
FDL editor aliases :
simple-swap-test
Latex:
simple-swap-test(AModel;prog;i;j) ==
A-bind(AModel) (A-coerce(AModel) (A-fetch'(AModel) i))
(\mlambda{}in@i.(A-bind(AModel) (A-coerce(AModel) (A-fetch'(AModel) j))
(\mlambda{}in@j.(A-bind(AModel) prog
(\mlambda{}x.(A-bind(AModel) (A-coerce(AModel) (A-fetch'(AModel) i))
(\mlambda{}out@i.(A-bind(AModel) (A-coerce(AModel) (A-fetch'(AModel) j))
(\mlambda{}out@j.(A-return(AModel)
((out@i =\msubz{} in@j) \mwedge{}\msubb{} (out@j =\msubz{} in@i))))))))))))
Date html generated:
2016_05_15-PM-02_19_39
Last ObjectModification:
2015_09_23-AM-07_38_40
Theory : monads
Home
Index