* Re: [Oktoberfest 2017] Sad news: Kosta Dosen
@ 2017-10-29 14:37 1337777.OOO
0 siblings, 0 replies; only message in thread
From: 1337777.OOO @ 2017-10-29 14:37 UTC (permalink / raw)
To: psh, categories, coq-club, types-list; +Cc: Steve Awodey
Proph
https://gitlab.com/1337777/dosen/blob/master/dosenSolution101.v
solves some question of Dosen which is how to program the
logical/particular/rewriting/(one-step) polymorphism/cut-elimination
and the confluence/commutation of this rewriting for the grammatical
polymorph pairing-projections ( "product" ) ...
The computational/total/asymptotic/reduction/(multi-step)
polymorphism/cut-elimination of many polymorph mathematics were
already programmed in the earlier COQ texts : polymorph
reflections/adjunctions , polymorph comonad , polymorph
grammatical-metafunctors , polymorph localizations ... The form of
these programs was the same : primo to define grammatical (multi-step)
reduction relation , then secondo to define some non-structural
recursive grade function from the morphisms to the integers , and
finally tertio to define some non-structural recursive cut-elimination
function from any two-morphisms input ( "topmost cut" ) by choosing
some syntactic-match cases precedence when there are ambiguities ref
which reduction shall apply . Memo that the grade function was linear
arithmetic ( addition , maximum , less than ) over the integers .
Now to proceed to the logical consequences of such things shall
require some alternative logical description : some
logical/particular/rewriting/(one-step) polymorphism/cut-elimination
resolution and the confluence/commutation lemma of this rewriting
which shows that this logical resolution is indeed some alternative
description of the computational function . Memo that the grade
function here will ( necessarily ? ) be non-linear arithmetic (
addition , multiplication , distributivity , less than ) over the
integers which mimic/simulate the constructors of the morphisms , in
particular : the polymorphism ( "distributivity" ) of the
composition/cut constructor over the pairing constructor . More
precisely : grade ( f o> g ) = 3 * grade f * grade g ; grade ( 1 ) =
1 ; grade ( ~_1 o> f ) = 1 + grade f ; grade ( ~_2 o> f ) = 1 +
grade f ; grade ( << f , g >> ) = 1 + grade f + grade g .
This COQ program and deduction is mostly-automated , and the COQ [nia]
automation-tactic is sufficient for this non-linear arithmetic . The
confluence lemma produce some total of ( ( 7 * 8 ) * ( 7 * 8 ) = 3136
goals ) , but only ( 37 classes of goals) are critical via the
automation-tactics ; moreover the COQ computer ( parallel dual core ,
4 gigabytes memory ) motion-time for ( 93 + 27 = 120 minutes ) .
For instant first impression , the lemma that the « resolved-cut » is
congruent modulo solution-conversion is written as :
#+BEGIN_EXAMPLE
Fixpoint solveCoMod_PolyCoMod_cong_Post_ len {struct len} :
forall (B1 : obCoMod) (B1' : obCoMod) (g'Sol g'Sol0 : 'CoMod(0 B1 ~>
B1' )0 %sol)
( Hconv : ( g'Sol0 ~~~ g'Sol )%sol_once ),
forall B2 (g_Sol : 'CoMod(0 B2 ~> B1 )0 %sol),
forall (H_gradeParticular : ( (Sol.gradeConv Hconv +
Rewrite.gradeParticular ((Sol.toCoMod g_Sol) o>CoMod (Sol.toCoMod
g'Sol))%poly)%Z <= Z.of_nat len)%Z ),
( ( ( g_Sol o>CoMod g'Sol0 ) ~~~ ( g_Sol o>CoMod g'Sol ) ))
%sol %sol_conv .
#+END_EXAMPLE
This file [[1337777.OOO//dosenSolution101.v]] is the epilogue of Dosen
book « Cut-Elimination in Categories » .
Keywords : 1337777.OOO//dosenSolution101.v ; pairing-projections
grammar ; logical cut-elimination ; confluence ; non-linear arithmetic
Outline :
* Grammatical description of polymorph pairing-projections
** Importing the non-linear arithmetic COQ automation-tactics
** Common-inductive polymorph morphisms, with overloaded notations
for the composition/cut constructor
* Solution
** Grade of solution-conversion for combined non-structural induction
** Destruction of solution-morphisms with inner-instantiation of
object-indexes
* Congruent-Rewriting relation
** Non-linear mimicking grade function
** Degradation lemma and the non-linear arithmetic COQ automation-tactic [nia]
* Polymorphism/cut-elimination by congruent-rewriting
* Confluence
** Goals accounting
** Unique solution for the logical-rewriting relation
* Polymorphism conversion
** Cut-elimination resolution is congruent from the
polymorphism-terminology to the solution-terminology
-----
PS : Oktoberfest 2017 continues as NovemberSchätz 2017 at the CMU
Schätz weekends 11:37-14:00 until november ...
-----
memory amazon.com/hz/wishlist/ls/28SN02HR4EB8W , eth
0x54810dcb93b37DBE874694407f78959Fa222D920 , paypal
1337777.OOO@gmail.com , wechatpay 2796386464@qq.com , irc #OOO1337777
^ permalink raw reply [flat|nested] only message in thread
only message in thread, other threads:[~2017-10-29 14:37 UTC | newest]
Thread overview: (only message) (download: mbox.gz / follow: Atom feed)
-- links below jump to the message on this page --
2017-10-29 14:37 [Oktoberfest 2017] Sad news: Kosta Dosen 1337777.OOO
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox;
as well as URLs for NNTP newsgroup(s).