The Coq mailing list

["1337777.OOO" <1337777.ooo AT gmail.com>]

Proph

https://gitlab.com/1337777/cartier/blob/master/cartierSolution2.v

solves half of some question of Cartier which is how to program
grammatical meta (metafunctors) ...

Outline : Primo, it is sufficient for now to touch only
product-preserving retractive reflection into subgraph instead of
metafunctors-grammar localization ( <=> "Galois-topology"  <=>
"universal closure operations" <=?> "calculus of fractions" <=>
"special factorization systems" ); the case of finite-limit will
require some new elimination-scheme (?diaconescu-scheme?) which may
still-be avoided for the purely-computational questions : the cone
property and pairing-through-the-limit-subobject property are
corresponding logical properties/invariants which may be erased.
Secondo, it is possible for now to verify by pencil-and-paper (+) that
these terminating reduction relations satisfy local confluence
(commutation of basic reductions) by discovering-and-appending
whatever derivable solution-conversions lemma are needed and (++) that
this solution terminology permit the derivability of the
associativity-conversion. Therefore relative-decidability of the
(data) coherence question (sameness-of-arrows) will follow from this
cut-elimination, although the (logical) theoremhood question
(presence-of-arrow) is lost. Tertio, the coreflection (right adjoint)
is some (invisible) inclusion functor, such that the reflection is
some endofunctor inside one single graph. Also the
reverse-isomorphisms for expressing the retraction (reversibility of
the counit-morphism and more) and the product-preservation
(reversibility of those pairings-morphisms which arise from the known
computation of the product inside the subreflective subgraph) are
explicit data :

| ( 'RevCoUnit o>Mod (f : 'CoMod(0 Reflection0 (Reflection0 A1) ~>
Reflection0 A2 )0) )   :   'CoMod(0 Reflection0 A1 ~> Reflection0 A2
)0

| ( (f : 'CoMod(0 Reflection0 L ~> Reflection0 (Limit (Reflection0 A1)
(Reflection0 A2)) )0) o>Mod 'RevLimit1Unit )   :   'CoMod(0
Reflection0 L ~> Reflection0 (Limit A1 A2) )0

Quarto, the resolution/cut-elimination now proceeds by two phases :
(+) first into some intermediate-solution, where only the
subgraph-projection morphisms are eliminated and (++) then into some
final-solution where also the subgraph-pairing morphisms are
eliminated. Again the formulation is such that all the senses/semantic
of « product-preserving retractive reflection » is still-expressible
in the terminology of the solution, and any more needed derivable
solution-conversion will be discovered-and-appended during the local
confluence deduction. And the degradation lemma is more technical :
(+) the choice of the grades for the morphisms is more constrained
such that some two-phases-resolution is now required (++) and for the
pairings-morphisms, on shall require simultaneous/parametric full
reduction of every reductible morphisms in the pairings. This COQ
program and deduction is mostly automated, and is necessary instead of
pencil-and-paper if there are no prior expectations.

Keywords : 1337777.OOO//cartierSolution2.v ; metafunctors-grammar ; 
localization

POSTSCRIPT : the earlier file [[1337777.OOO//cartierSolution.v]] shall
not have the hidden cut PolyMetaTransf in the final solution, for sure
:

| View1 a : 'Modos(0 (View0 A) ~> (View0 A') )0

| PolyMetaFunctor func1 x : 'Modos(0 (View0 A) ~> (MetaFunctor func1) )0)

| f o>Modos_ transf : 'Modos(0 (View0 A) ~> (MetaFunctor func'1) )0)

| [[ v_ ]] : 'Modos(0 (MetaFunctor func1) ~> F )0


-----8<-----

Breaking News :

https://gitlab.com/1337777/maclane/blob/master/maclaneSolution.svg

shows how my mom has discovered "independently" that her associations
pentagon is some recursive square (word-normalization functor). Now
will you (yes, you) cite my mom ?


----->8-----

Proph

http://ethereum.github.io/browser-solidity/#gist=89b4ee8d3ee4e50299323ed2c6305daf
http://swarm-gateways.net/bzz:/0eb425a28278cec83a76ed1fe924f777cab9c81417846a598416d76a1da30acf

solves my earlier question which is how to measure reviews/citations
by using public programmatic proxy-authors « pprogxy » ( "ethereum
blockchain cryptographic smart-contract" ) ; and also calls-for-papers
[CFP] for the "formal verification" of these pprogxies , where the
chosen reviews/citations-metric is through these same pprogxies !?1!

Outline : Primo, "review" and "citation" is the same thing and shall
be costly and is similar to some current/currency/token. Secondo, the
question of initialization (which is external) shall be de-coupled
from the question of logic/current (which is internal) : the current
is viewed through both basic-marketmulti-initialization and
inductive/recursive/feedback-initialization. Tertio, reviews/citations
is similar to some current/currency/token which flows downward from
younger document-nodes to older document-nodes (which may refuse to
receive/stake some too-diluted citation/token). Any document-node
("editor") which lastly-possesses some tokens, may sink/burn/erase
these tokens into another upward (younger) document-node ("author"),
which may mint/create/faucet only-half of those sinked-tokens on
behalf of any other newly-created document-node ("reviewer")
citing/towards it. Some record of all these transactions (sink or
faucet or cite or mere-transfer) is memorized via internal storage and
external log/trace events, such that after inputing some
dilution-percentage of initially-sinked tokens at existing
document-nodes then oneself may compute the dilution-percentage of the
balance at each document-node and may compute the real-measure (ratio
of sinked diluted-tokens over fauceted diluted-tokens) at each
document-node. Finally some archive tool may integrate the common
metadata content-address ("SHA hash") of each document-node along
another content-addressable replicated-storage tool ("swarm DHT").

Alternative : Another initialization may simply-be to assume that the
user-addresses (from some constant list) who own document-nodes are
non-interdependent and then either (+) to prevent self-citation or (+)
to limit the total number of new document-nodes created by each
particular user-address (and later
externally-iteratively/inductive-update these particular numbers). But
non-interdependence is rare :
[[http://retractionwatch.com/2017/08/22/one-way-boost-unis-ranking-ask-faculty-cite/]]
[[https://scholarlykitchen.sspnet.org/2017/08/03/transparent-peer-review-mean-important/]]
... and it is common that reviewers flip-flop between : (
monetarist-or-tribalistic ) « possibility » ( "discretion" )   versus
 ( monetarist-or-tribalistic ) « copy-me grade » ( "CV" , "objective"
, refuse to be subjective-under-teaching ) ...

Formal verification : There are many alternatives from attempting to
verify the intermediate-level assembly code. Primo, the transactions
basic-accounting may be verified, where the high-level source-code
already-is the specification. Secondo, the complex mathematical
algorithms may be verified, where this verification is no-longer
particular to the ethereum-virtual-machine. Tertio, that the hidden
high-level source-code does compile to the public
ethereum-virtual-machine-opcode/bytecode stored inside the blockchain,
may be verified simply-by making this high-level source-code public.
Quarto, practical-engineering hacks/sidechannels may only be
verified-and-corrected over some long-time testing with
smaller-stakes.

EASY REGISTRATION : Primo, download Chrome Metamask extension
[[google.com/#q=Chrome+Metamask]] , select "Ropsten Test Net" , create
new key , click "Buy" to get test tokens. Secondo, in the above
"Browser Solidity" source-code page , select "Injected Web3"
Environment , parse/compile and click "At Address for ¢entseCurrent"
and input : 0xc7c6a7b7d396388127ce6140b39ca1eff3beb07b . Tertio, post
the new review text in the above "Swarm Gateways" and get the
content-address hash. Quarto, register this review metadata as some
new pprogxy for the Centse currency.


-----

eth 0x54810dcb93b37DBE874694407f78959Fa222D920 , paypal
1337777.OOO AT gmail.com
 , wechatpay 
2796386464 AT qq.com
 , irc #OOO1337777