Skip to content

Instantly share code, notes, and snippets.

@jonsterling

jonsterling/gist:6bed2d3327b83d071ab397d290b6e1db

Last active September 20, 2018 02:57
Show Gist options
  • Save jonsterling/6bed2d3327b83d071ab397d290b6e1db to your computer and use it in GitHub Desktop.
Save jonsterling/6bed2d3327b83d071ab397d290b6e1db to your computer and use it in GitHub Desktop.
Download ZIP
Raw
gistfile1.txt
Core RedML is (so far) a one-sided, polarized L calculus in the style of Curien-Herbelin-Munch.
Lambda calculus can be compiled to Core RedML through a bunch of gnarly macros. For instance, the term
(((lam [x] (lam [y] (pair x y))) nil) nil)
should evaluate to a pair of nils. This term is compiled into Core RedML as the first stage of the following
computation trace, which shows how it computes to the desired pair.
State: (cut
(μ [%12]
(cut
(μ [%9]
(cut
{(split [in x] [out %3]
(cut
{(split [in y] [out %5]
(cut
(μ [%6]
(cut x (μ [%7] (cut y (μ [%8] (cut ([0 %7] [1 %8]) %6))))))
%5))}
%3))}
(force {%10} (cut () (μ [%11] (cut %10 ([in %11] [out %9])))))))
(force {%13} (cut () (μ [%14] (cut %13 ([in %14] [out %12])))))))
stop)
State: (cut
(μ [%9]
(cut
{(split [in x] [out %3]
(cut
{(split [in y] [out %5]
(cut
(μ [%6]
(cut x (μ [%7] (cut y (μ [%8] (cut ([0 %7] [1 %8]) %6))))))
%5))}
%3))}
(force {%10} (cut () (μ [%11] (cut %10 ([in %11] [out %9])))))))
(force {%13} (cut () (μ [%14] (cut %13 ([in %14] [out stop]))))))
State: (cut
{(split [in x] [out %3]
(cut
{(split [in y] [out %5]
(cut
(μ [%6]
(cut x (μ [%7] (cut y (μ [%8] (cut ([0 %7] [1 %8]) %6))))))
%5))}
%3))}
(force {%10}
(cut
()
(μ [%11]
(cut
%10
([in %11]
[out (force {%13}
(cut () (μ [%14] (cut %13 ([in %14] [out stop])))))]))))))
State: (cut
()
(μ [%11]
(cut
(split [in x] [out %3]
(cut
{(split [in y] [out %5]
(cut
(μ [%6]
(cut x (μ [%7] (cut y (μ [%8] (cut ([0 %7] [1 %8]) %6))))))
%5))}
%3))
([in %11]
[out (force {%13}
(cut () (μ [%14] (cut %13 ([in %14] [out stop])))))]))))
State: (cut
(split [in x] [out %3]
(cut
{(split [in y] [out %5]
(cut
(μ [%6]
(cut x (μ [%7] (cut y (μ [%8] (cut ([0 %7] [1 %8]) %6))))))
%5))}
%3))
([in ()]
[out (force {%13} (cut () (μ [%14] (cut %13 ([in %14] [out stop])))))]))
State: (cut
(split [in x] [out %3]
(cut
{(split [in y] [out %5]
(cut
(μ [%6]
(cut x (μ [%7] (cut y (μ [%8] (cut ([0 %7] [1 %8]) %6))))))
%5))}
%3))
([in ()]
[out (force {%13} (cut () (μ [%14] (cut %13 ([in %14] [out stop])))))]))
State: (cut
{(split [in y] [out %5]
(cut
(μ [%6] (cut () (μ [%7] (cut y (μ [%8] (cut ([0 %7] [1 %8]) %6))))))
%5))}
(force {%13} (cut () (μ [%14] (cut %13 ([in %14] [out stop]))))))
State: (cut
{(split [in y] [out %5]
(cut
(μ [%6] (cut () (μ [%7] (cut y (μ [%8] (cut ([0 %7] [1 %8]) %6))))))
%5))}
(force {%13} (cut () (μ [%14] (cut %13 ([in %14] [out stop]))))))
State: (cut
{(split [in y] [out %5]
(cut
(μ [%6] (cut () (μ [%7] (cut y (μ [%8] (cut ([0 %7] [1 %8]) %6))))))
%5))}
(force {%13} (cut () (μ [%14] (cut %13 ([in %14] [out stop]))))))
State: (cut
()
(μ [%14]
(cut
(split [in y] [out %5]
(cut
(μ [%6]
(cut () (μ [%7] (cut y (μ [%8] (cut ([0 %7] [1 %8]) %6))))))
%5))
([in %14] [out stop]))))
State: (cut
(split [in y] [out %5]
(cut
(μ [%6] (cut () (μ [%7] (cut y (μ [%8] (cut ([0 %7] [1 %8]) %6))))))
%5))
([in ()] [out stop]))
State: (cut
(split [in y] [out %5]
(cut
(μ [%6] (cut () (μ [%7] (cut y (μ [%8] (cut ([0 %7] [1 %8]) %6))))))
%5))
([in ()] [out stop]))
State: (cut
(μ [%6] (cut () (μ [%7] (cut () (μ [%8] (cut ([0 %7] [1 %8]) %6))))))
stop)
State: (cut
(μ [%6] (cut () (μ [%7] (cut () (μ [%8] (cut ([0 %7] [1 %8]) %6))))))
stop)
State: (cut
(μ [%6] (cut () (μ [%7] (cut () (μ [%8] (cut ([0 %7] [1 %8]) %6))))))
stop)
State: (cut () (μ [%7] (cut () (μ [%8] (cut ([0 %7] [1 %8]) stop)))))
State: (cut () (μ [%8] (cut ([0 ()] [1 %8]) stop)))
State: (cut ([0 ()] [1 ()]) stop)
State: (cut ([0 ()] [1 ()]) stop)
Final: (cut ([0 ()] [1 ()]) stop)
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment