Закрытое открытое понимание символа рекурсии

Question

Этот вопрос напрямую не о том, что является открытой или закрытой рекурсией, как мы могли видеть на этом вопросе, но более конкретно о этом разговоре , на который ссылаются во многих местах.

Внутри мы можем видеть выражение, такое как:

(fun(x1:τ1)⇒e)⇓(fun(x1:τ1)⇒e)

Мой вопрос: что означает ⇓?

Я просматривал этот интернет и не сделалнашел что-то особенное в этом, принимая во внимание, что поиск символа всегда утомителен.

Answer 1

Не уверен, ответит ли он на ваш вопрос, но, читая различные материалы в Интернете, я думаю, ⇓ означает, что оценивается как или , уменьшено до .

Для выражения:

(fun(x1:τ1)⇒e)⇓(fun(x1:τ1)⇒e)

это означает, что функция fun, которая принимает x1 типа τ1 в качестве аргумента, может быть уменьшена до той же функции.

Может быть этот вопрос на SE может помочь вам.