Skip to content

Instantly share code, notes, and snippets.

@cartazio
Created February 18, 2020 19:55
Show Gist options
  • Star 0 You must be signed in to star a gist
  • Fork 0 You must be signed in to fork a gist
  • Save cartazio/8b7ff3f5ba2af2c4690e25ed4241982d to your computer and use it in GitHub Desktop.
Save cartazio/8b7ff3f5ba2af2c4690e25ed4241982d to your computer and use it in GitHub Desktop.
d/dx (x ^ a) == d/dx (a -> x )
we never consider a ^ x === x -> a ()
log_x(\nu Y -> T) == \mu Z -> log_X T , where Z == log_X Y
(translation: every time we see log_X Y , in T, replace taht with Z )
F === Y |-> X * Y
Stream X == \nu (F ) == \nu Y |-> X * Y
log_X (Stream X) == log_X (\nu F) == log_X (\nu Y |-> X * Y)
log and fixpoint exchange
== \mu (W |-> log_X (X * W)) == \mu (W |-> log_X(X) + Log_X(W) ) == \mu (W |-> 1 + log_X W )
replaced W
codata Stream x = x * Stream x
codata LogCo x = Log_x (Stream x) ==
type LogCo = x |-> Log_x (Stream x)
== x |-> Log_x (\NUUU Y |-> x * Y)
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment