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