[Top][All Lists]

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Re: if vs. when vs. and: style question

From: Stefan Monnier
Subject: Re: if vs. when vs. and: style question
Date: Sun, 29 Mar 2015 20:09:48 -0400
User-agent: Gnus/5.13 (Gnus v5.13) Emacs/25.0.50 (gnu/linux)

> What is α?  What is β?

> Wouldn't have it been better to name those variables number-of-rows
> or tree-height or some other words denoting their actual meaning?

Usually, within the context where the mathematical formula is used,
these variables *are* names denoting their meaning.  These depend on
notational conventions used within specific communities (and usually not
formalized), but they are convenient.  So instead of

    has_type env exp type

you say

    Γ ⊢ e : τ

and it is just as explicit, because τ does mean "a type", and Γ means "a
type environment", and ":" means "has type", and "⊢" means "based on
hypotheses such and such".  Some of those letters/signs have meaning
shared within a fairly large mathematical community while others are
much more specific to a specialized subfield.

Of course, if you're not familiar with the local conventions, it looks
like line noise, but otherwise it offers people much higher concision,
so they can focus on the important aspects.


reply via email to

[Prev in Thread] Current Thread [Next in Thread]