James/tricu
1
1
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity

Updates to demos

Browse Source
This commit is contained in:
James Eversole
2025-04-16 14:23:53 -05:00
parent 25bfe139e8
commit b8e2743103
7 changed files with 61 additions and 39 deletions
Download Patch File Download Diff File Expand all files Collapse all files

15
demos/equality.tri
View File

@ -12,19 +12,16 @@ not_TC? = t (t (t t) (t t t)) (t t (t t t))
-- /demos/toSource.tri contains an explanation of `triage`
demo_triage = a b c : t (t a b) c
demo_matchBool = (ot of : demo_triage
of
(_ : ot)
(_ _ : ot)
)
demo_matchBool = a b : demo_triage b (_ : a) (_ _ : a)
-- Lambda representation of the Boolean `not` function
not_Lambda? = demo_matchBool demo_false demo_true
-- Since tricu eliminates Lambda terms to SKI combinators, the tree form of many
-- As tricu eliminates Lambda terms to SKI combinators, the tree form of many
-- functions defined via Lambda terms are larger than the most efficient TC
-- representation. Between different languages that evaluate to tree calculus
-- terms, the exact implementation of Lambda elimination may differ and lead
-- to different tree representations even if they share extensional behavior.
-- representation possible. Between different languages that evaluate to tree
-- calculus terms, the exact implementation of Lambda elimination may differ
-- and lead to different trees even if they share extensional behavior.
-- Let's see if these are the same:
lambdaEqualsTC = equal? not_TC? not_Lambda?