tricu

An interpreted language for exploring Tree Calculus
Log | Files | Refs | README | LICENSE

d14168490eeb3a4bab3c431d4ae936c51ead54e4e7155d9dded065442f2b9da0.tri (1289B)

      1 !import prelude *
      2 !export *
      3 
      4 main = lambdaEqualsTC
      5 
      6 -- We represent `false` with a Leaf and `true` with a Stem Leaf
      7 demo_false = t
      8 demo_true  = t t
      9 
     10 -- Tree Calculus representation of the Boolean `not` function
     11 not_TC?     = t (t (t t) (t t t)) (t t (t t t))
     12 
     13 -- /demos/toSource.tri contains an explanation of `triage`
     14 demo_triage = a b c : t (t a b) c
     15 demo_matchBool = a b : demo_triage b (_ : a) (_ _ : a)
     16 
     17 -- Lambda representation of the Boolean `not` function
     18 not_Lambda? = demo_matchBool demo_false demo_true
     19 
     20 -- As tricu eliminates Lambda terms to SKI combinators, the tree form of many
     21 -- functions defined via Lambda terms are larger than the most efficient TC
     22 -- representation possible. Between different languages that evaluate to tree
     23 -- calculus terms, the exact implementation of Lambda elimination may differ
     24 -- and lead to different trees even if they share extensional behavior.
     25 
     26 -- Let's see if these are the same:
     27 lambdaEqualsTC = equal? not_TC? not_Lambda?
     28 
     29 -- Here are some checks to verify their extensional behavior is the same:
     30 true_TC?  = not_TC? demo_false
     31 false_TC? = not_TC? demo_true
     32 
     33 true_Lambda?  = not_Lambda? demo_false
     34 false_Lambda? = not_Lambda? demo_true
     35 
     36 bothTrueEqual?  = equal? true_TC?  true_Lambda?
     37 bothFalseEqual? = equal? false_TC? false_Lambda?