3
$\begingroup$

What does the symbol "$\triangleright$" mean programming language semantics? I've seen it in the context of datatypes in and the evaluation of expressions in environments.

For example :

$$tenv \triangleright erht \implies tval $$

or

$$tenv[tval/x]\triangleright ebody\implies t\,.$$

Here, $tenv$ is an environment and $ebody$ is the body of some expression.

Improve this question
$\endgroup$
3
  • 1
    $\begingroup$ @DavidRicherby The context is the one of data types and evaluation into an environment. In the second example tenv is an environment and **ebody ** is the body of an expression $\endgroup$ – user43288 Dec 7 '16 at 19:12
  • 4
    $\begingroup$ This symbol is used in different ways in different contexts in CS, for example in term rewriting, I've seen it represent "is a super-term". Here it sure looks like $e\triangleright t\Rightarrow v$ means "$t$ reduces to $v$ in environment $e$". $\endgroup$ – cody Dec 7 '16 at 21:14
  • $\begingroup$ @GerardoZinno More generally, whatever you're reading should be telling you what it means (or rather what the whole $- \triangleright - \implies -$ relation means). This notation is not "standardized" in any way. You may find my answer (cs.stackexchange.com/questions/54508/…) useful, and it should help clarify what I mean. $\endgroup$ – Derek Elkins left SE Dec 8 '16 at 6:46
3
$\begingroup$

Most probably, in your context, ▹ is just a syntactic separator, meaning "in the environment to the left of ▹, the formula to the right of ▹ holds".

However, ▹ has no fixed meaning in general. I used it myself with completely different definitions.

Improve this answer
$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy