equality.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?