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

Immutable definitions and documentation updates

Browse Source
This commit is contained in:
James Eversole
2025-01-24 16:14:33 -06:00
committed by James Eversole
parent 88b1c71695
commit 3175132eec
6 changed files with 137 additions and 32 deletions
Download Patch File Download Diff File Expand all files Collapse all files

31
demos/equality.tri
View File

@ -1,24 +1,35 @@
-- We represent `false` with a Leaf and `true` with a Stem Leaf
false = t
true = t t
triage = (\a b c : t (t a b) c)
-- Tree Calculus representation of the Boolean `not` function
not_TC? = t (t (t t) (t t t)) (t t (t t t))
-- /demos/toSource.tri contains an explanation of `triage`
triage = (\a b c : t (t a b) c)
matchBool = (\ot of : triage
of
(\_ : ot)
(\_ _ : ot)
)
not_TC? = t (t (t t) (t t t)) (t t (t t t))
-- Lambda representation of the Boolean `not` function
not_Lambda? = matchBool false true
areEqual? = equal not_TC not_Lambda
-- Since 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.
true_TC? = not_TC false
false_TC? = not_TC true
-- Let's see if these are the same:
lambdaEqualsTC = equal? not_TC? not_Lambda?
true_Lambda? = not_Lambda false
false_Lambda? = not_Lambda true
-- Here are some checks to verify their extensional behavior is the same:
true_TC? = not_TC? false
false_TC? = not_TC? true
areTrueEqual? = equal true_TC true_Lambda
areFalseEqual? = equal false_TC false_Lambda
true_Lambda? = not_Lambda? false
false_Lambda? = not_Lambda? true
bothTrueEqual? = equal? true_TC? true_Lambda?
bothFalseEqual? = equal? false_TC? false_Lambda?

12
demos/toSource.tri
View File

@ -2,13 +2,13 @@
-- even if it's a function. This includes lambdas which are eliminated to
-- Tree Calculus (TC) terms during evaluation.
-- Triage takes four arguments: the first three represent behaviors for each
-- `triage` takes four arguments: the first three represent behaviors for each
-- structural case in Tree Calculus (Leaf, Stem, and Fork).
-- The fourth argument is the value whose structure is inspected. By evaluating
-- the Tree Calculus term, `triage` enables branching logic based on the term's
-- shape, making it possible to perform structure-specific operations such as
-- reconstructing the terms' source code representation.
triage = (\a b c : t (t a b) c)
triage = (\leaf stem fork : t (t leaf stem) fork)
-- Base case of a single Leaf
sourceLeaf = t (head "t")
@ -34,13 +34,13 @@ sourceFork = (\convert : (\a b rest :
-- Wrapper around triage
toSource_ = y (\self arg :
triage
sourceLeaf -- Triage `a` case, Leaf
(sourceStem self) -- Triage `b` case, Stem
(sourceFork self) -- Triage `c` case, Fork
sourceLeaf -- `triage` "a" case, Leaf
(sourceStem self) -- `triage` "b" case, Stem
(sourceFork self) -- `triage` "c" case, Fork
arg) -- The term to be inspected
-- toSource takes a single TC term and returns a String
toSource = (\v : toSource_ v "")
exampleOne = toSource true -- OUT: "(t t)"
exampleTwo = toSource not? -- OUT: "(t (t (t t) (t t t)) (t t (t t t)))"
exampleTwo = toSource not? -- OUT: "(t (t (t t) (t t t)) (t t (t t t)))"