This question is not directly about what is open or closed recursion as we could see on this question, but it's more specifically about this talk which is referenced in many placed.
Inside we can see expression such as:
(fun(x1:τ1)⇒e)⇓(fun(x1:τ1)⇒e)
My question is: what does the ⇓
stand for?
I looked around this internet and didn't found anything particular about that, taking into account that googling a symbol is always tedious.
Not sure if it does answer your question, but from reading various material online I think ⇓
means evaluates to or reduced to.
For expression:
(fun(x1:τ1)⇒e)⇓(fun(x1:τ1)⇒e)
it means, function fun
which takes x1
of type τ1
as an argument can be reduced to the same function.
May be this question on SE might help you.