VictorTaelin/Interaction-Calculus

typo in 2nd diagram (of commutation law)

tribbloid opened this issue · 1 comments

original:

   Lambda Application                         Pair Application
                                                                  
   let {a b} = (λx body) in cont             ({fst snd} arg)   
   ------------------------------             ---------------
   a <- (λx0 b0)                             let {x0 x1} = arg in
   b <- (λx1 b1)                             {(fst x0) (snd x1)}
   x <- {x0 x1}
   let {b0 b1} = body in
   cont                   
       
    ret  arg         ret  arg            ret  arg         ret  arg  
     |   |            |    |              |   |            |    |   
     |___|            |    |              |___|            |    |   
 let  \#/            /_\  /_\         app  \ /            /#\  /#\  
       |      ==>    |  \/  |               |      ==>    |  \/  |  
       |             |_ /\ _|               |             |_ /\ _|  
 lam  /_\            \#/  \#/        pair  /#\            \ /  \ /  
     |   |            |    |              |   |            |    |   
     |   |            |    |              |   |            |    |   
     x  body          x   body           var body         var  body 

 "The projection of a lambda         "The application of a pair is a pair
 substitutes the projected vars      of the first element and the second
 by a copies of the lambda that      element applied to projections of the
 return its projected body, with     application argument."
 the bound variable substituted
 by the new lambda vars paired."

should be:

   Lambda Duplication                         Pair Application
                                                                  
   let {a b} = (λx body) in cont             ({fst snd} arg)   
   ------------------------------             ---------------
   a <- (λx0 b0)                             let {x0 x1} = arg in
   b <- (λx1 b1)                             {(fst x0) (snd x1)}
   x <- {x0 x1}
   let {b0 b1} = body in
   cont                   
       
     a   b            a    b             ret  arg         ret  arg  
     |   |            |    |              |   |            |    |   
     |___|            |    |              |___|            |    |   
 let  \#/            /_\  /_\         app  \ /            /#\  /#\  
       |      ==>    |  \/  |               |      ==>    |  \/  |  
       |             |_ /\ _|               |             |_ /\ _|  
 lam  /_\            \#/  \#/        pair  /#\            \ /  \ /  
     |   |            |    |              |   |            |    |   
     |   |            |    |              |   |            |    |   
     x  body          x   body           fst snd          fst  snd  

 "The projection of a lambda         "The application of a pair is a pair
 substitutes the projected vars      of the first element and the second
 by a copies of the lambda that      element applied to projections of the
 return its projected body, with     application argument."
 the bound variable substituted
 by the new lambda vars paired."

I also realised that any reference to "superposition" or "node labelling/coloring" has been removed in HVM2, should this doc be considered obsolete?