Search code examples
recursionprogramming-languagescomputer-sciencenotation

Closed an open recursion symbol understanding


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.


Solution

  • 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.