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

Background predicates don't appear as conditionals in laws #46

Open
isovector opened this issue Jun 16, 2020 · 0 comments
Open

Background predicates don't appear as conditionals in laws #46

isovector opened this issue Jun 16, 2020 · 0 comments

Comments

@isovector
Copy link
Contributor

isovector commented Jun 16, 2020

Consider the original sig, with _contains in the signature proper:

== Functions ==                                                                                                 
withReply :: Thread -> Thread -> Thread                                                                         
     True :: Bool                                                                                               
                                                                                                                
== Functions ==                                                                                                 
  comment :: Post -> Thread                                                                                     
     lock :: Thread -> Thread                                                                                   
  replyTo :: Post -> Thread -> Thread -> Thread                                                                 
_contains :: Post -> Thread -> Bool                                                                             
                                                                                                                
== Laws ==                                                                                                      
  1. lock (lock t) = lock t                                                                                     
  2. _contains p (comment p2) = _contains p2 (comment p)                                                        
  3. _contains p (comment p)                                                                                    
  4. _contains p (lock t) = _contains p t                                                                       
  5. withReply (lock t) t2 = lock t                                                                             
  6. _contains p (withReply t t) = _contains p t                                                                
  7. replyTo p t (comment p) = withReply (comment p) t                                                          
  8. replyTo p t (lock t2) = lock t2                                                                            
  9. _contains p t => _contains p (withReply t t2)                                                              
 10. _contains p (replyTo p2 t t2) = _contains p t2                                                             
 11. replyTo p (comment p2) (comment p2) = replyTo p (comment p) (comment p2)                                   
 12. _contains p t2 => replyTo p t (withReply t2 t) = withReply (replyTo p t t2) t                              
 13. _contains p (withReply t (lock t2)) = _contains p (withReply t t2)                                         
 14. _contains p3 t & _contains p2 t2 => _contains p (withReply t (comment p2)) = _contains p (withReply t t2)  
 15. _contains p t2 => _contains p (withReply t (comment p)) = _contains p (withReply t t2)                     
 16. _contains p t4 => replyTo p t (replyTo p2 t2 t3) = replyTo p2 t2 (replyTo p t t3)                          
 17. _contains p2 t5 & _contains p3 t2 => replyTo p (replyTo p2 t t2) t3 = replyTo p (replyTo p2 t4 t2) t3      
 18. _contains p2 t4 & _contains p4 t2 & _contains p3 t5 => replyTo p (replyTo p2 t t2) t3 = replyTo p (replyTo 
p3 t t2) t3                                                                                                     
 19. _contains p (withReply t (withReply t t2)) = _contains p (withReply t t2)                                  
 20. _contains p (withReply t (withReply t2 t)) = _contains p (withReply t t2)                                  
 21. _contains p (withReply t (withReply t2 t2)) = _contains p (withReply t t2)                                 
 22. _contains p (withReply (withReply t t2) t3) = _contains p (withReply t (withReply t3 t2))                  
 23. replyTo p t (withReply (comment p) t2) = withReply (withReply (comment p) t2) t                            
 24. replyTo p (lock (comment p2)) (comment p2) = replyTo p (lock (comment p)) (comment p2

but when it's moved to the background, we no longer see law 12 or similar laws with a _contains p t => precondition:

== Functions ==
withReply :: Thread -> Thread -> Thread
     True :: Bool
_contains :: Post -> Thread -> Bool

== Functions ==                    
comment :: Post -> Thread
   lock :: Thread -> Thread
replyTo :: Post -> Thread -> Thread -> Thread

== Laws ==
  1. lock (lock t) = lock t        
  2. _contains p (comment p2) = _contains p2 (comment p)
  3. _contains p (comment p)
  4. _contains p (lock t) = _contains p t
  5. withReply (lock t) t2 = lock t
  6. replyTo p t (comment p) = withReply (comment p) t
  7. replyTo p t (lock t2) = lock t2
  8. _contains p (replyTo p2 t t2) = _contains p t2
  9. replyTo p (comment p2) (comment p2) = replyTo p (comment p) (comment p2)
 10. _contains p (withReply t (lock t2)) = _contains p (withReply t t2)
 11. replyTo p t (withReply (comment p) t2) = withReply (withReply (comment p) t2) t
 12. replyTo p (lock (comment p2)) (comment p2) = replyTo p (lock (comment p)) (comment p2)
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