[INCLUDE TH/speedbar.blogme]
[SETFAVICON dednat4/dednat4-icon.png]
[# 
(defun c () (interactive) (find-blogme3-sh0-if "2007dnc-halfdnc"))
;;    http://angg.twu.net/2007dnc-halfdnc.html
;; file:///home/edrx/TH/L/2007dnc-halfdnc.html
#]
[lua:
  -- (eev-math-glyphs-edrx)
  eev_math_glyphs_edrx()
]
[lua: LR = R ]

[htmlize [J Half-DNC]


[WITHINDEX
[#
 #]
[RULE ----------------------------------------]

[tsec «half-DNC»  (to ".half-DNC")
[++N]. Half-DNC
===============
If we try to convert DNC terms and derivations
to standard (ð-calculus) terms and derivations
one step at a time, the intermediary terms will
lie "halfway between DNC and ð-calculus"; we say
that they are in "half-DNC".

Two examples of trees in half-DNC:
(between their DNC and ð-calculus counterparts)

        DNC:                     half-DNC:               ð-calculus:

[a]^1  [a|->b]^2           [a]^1  [a|->b]^2             [a]^1  [f]^2   
----------------           ----------------             ------------   
      b           b|->c        (a|->b)a       b|->c          fa        g
      -----------------        --------------------          -----------
              c                  (b|->c)((a|->b)a)              g(fa)  
            -----1             --------------------1          --------1        
            a|->c              ða.(b|->c)((a|->b)a)           ða.g(fa) 
     -----------------2   ------------------------------2   -----------2
     (a|->b)|->(a|->c)    (a|->b)|->ða.(b|->c)((a|->b)a)    ðf.ða.g(fa)  

         [a,b]^1                    [a,b]^1                   [p]^1         
         -------                    -------                   -----         
[a,b]^1     b     b|->c    [a,b]^1     b     b|->c   [p]^1     'p     g 
-------     -----------    -------     -----------   -------   --------- 
   a             c            a         (b|->c)b       p       g('p)   
   ---------------            ---------------          ---------------   
        a,c                     <a,(b|->c)b>             <p,g('p)>        
     ---------1              ------------------1       --------------1   
     a,b|->a,c               a,b|-><a,(b|->c)b>        ðp.<p,g('p)>    

Two examples of translations one step of a time:
(for the bottom terms of the two derivations)

                                            a,b|->a,c                
    (a|->b)|->(a|->c)                       a,b|-><a,c>              
    (a|->b)|->ða.c                          a,b|-><a,(b|->c)b>       
    (a|->b)|->ða.(b|->c)b                   a,b|-><a,(b|->c)('(a,b))>
    (a|->b)|->ða.(b|->c)((a|->b)a)     a,b|-><(a,b),(b|->c)('(a,b))>
    (a|->b)|->ða.(b|->c)((a|->b)a)     a,b|-><(a,b),g('(a,b))>     
           ðf.ða.(b|->c)(fa)          ð(a,b).<(a,b),g('(a,b))>     
           ðf.ða.g(fa)                    ðp.<p,g('p)>              
]

[tsec «half-DNC-dictionary»  (to ".half-DNC-dictionary")
[++N]. Half-DNC terms and the dictionary
========================================
Let's imagine that we have enlarged our dictionary
and now it also holds meanings for half-DNC terms.

Sometimes I think that the dictionary is just a
dictionary that I have constructed myself; my
dictionary, which is mine. So, if I want to add
an entry for a "term" whose name is an arbitrary
sequence of symbols, I can do that -

  "That's a great deal to make one word mean,"
  Alice said in a thoughtful tone.
  "When I make a word do a lot of work like that,"
  said Humpty Dumpty, "I always pay it extra."
  "Oh!" said Alice. She was too much puzzled to
  make any other remark. 

On the other hand, I want the dictionary to be as
coherent as possible - ideally it should be possible
to reconstruct all the meanings from the context...
]

[tsec «half-DNC-conventions»  (to ".half-DNC-conventions")
[++N]. Half-DNC: Some conventions
=================================
 and ' are used to indicate projections explicitly,
<,> is used to indicate pairing explicitly,
fa and ða.b are used to indicate application and
abstraction explicitly,
and the old implicit notations from DNC are still
allowed.

Note that in DNC all the "meanings" for the terms
are implicit and need to be retrieved from the
dictionary, but the types of the terms can be
reconstructed very easily.

In ð-calculus (with erased types) the meanings are
explicit, but the types may be hard(er) to
reconstruct.

Two examples:

   (a|->b)|->(a|->c)              
  ð(a|->b).ða.(b|->c)((a|->b)a)   
        ðf.ða.g(fa)               

   a,b|-><a,c>              	   
  ð(a,b).<(a,b),(b|->c)('(a,b))>
      ðp.<p,g('p)>              

Here the half-DNC terms are identical to the ð-terms -
all operations are explicit - but all the variables
with "complex types" have been renamed to long names
that reflext their types.
]

[tsec «half-dnc»  (to ".half-dnc")
[++N]. Half-DNC
===============
Take a DNC diagram describing some natural operation -
for example, the Currying adjunction.
Its bijection `<->' is an arrow `<-|' plus an arrow `|->',
plus that `<-|' and `|->' are inverses.

  a,b <=== a
   -       -
   |  <->  |
   v       v
   c ===> b|->c

The DNC diagram is intuitive to me.
I can look at it and say ``ok, this looks reasonable,
this diagram should be the right one''.
Now take the corresponding half-DNC diagram
(two squares - `<-|' and `|->').

      p <========= a       p <========= a
      -            -	   -            -
      |    <--|    |	   |    |-->    |
      v            v	   v            v
  f(p)('p) ===> f(a)	  c(p) ===> ðb.c(<a,b>)

    a:A|-f(a):B->C          p:A×B|-c(p):C
  -------------------     ---------------------
  p:AxB|-f(p)('p):C     a:A|-ðb.c(<a,b>):B->C

To me the half-DNC diagram looks much more formal.
I can't check it using just my intuition.
To arrive at it I start from the DNC diagram
and do a series of small translation steps.
If my dictionary is big enough then all the
partial translations will have meanings.
]


[tsec «translating-cat-diagrams»  (to ".translating-cat-diagrams")
[++N]. Translating categorical diagrams
=======================================

       a,b <=== a              a,b:A×B <=== a:A
        -       -      	         -           -
        |  <-|  |   |-------->   |    <-|    |
        v       v	         v           v
        c ==> b|->c	        c:C ==> b|->c:B->C
			                           /
            -		               -	     \
            |		               |	      v
            |		               |	         A×B <---| A
            |		               |	          -        -
            |		               |	      f^v |  <--|  | f
            v		               v	          v        v
			                                  C |---> B->C
     a,b <======= a	     p:A×B <========= a:A
      -           -	       -               -       	      -
      |    <--|   |   |- - >   |     <--|      |       	      .
      v           v	       v               v       	      .
  f(p)('p) ==> f(a)	  f(p)('p):C ==> f(a):B->C   	      .
						   /   	      .
						     \ 	      v
						      v
  					                 A×B <---| A
           				                  -        -
           				    ðp.f(p)('p) |  <--|  | f
           				                  v        v
           				                  C |---> B->C
]







]



]
[#
 # Local Variables:
 # coding: raw-text-unix
 # modes: (fundamental-mode blogme-mode)
 # End:
#]