Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

typo in 2nd diagram (of commutation law) #20

Open
tribbloid opened this issue Jun 5, 2024 · 1 comment
Open

typo in 2nd diagram (of commutation law) #20

tribbloid opened this issue Jun 5, 2024 · 1 comment

Comments

@tribbloid
Copy link

tribbloid commented Jun 5, 2024

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."
@tribbloid
Copy link
Author

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

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

1 participant