From mboxrd@z Thu Jan 1 00:00:00 1970 Path: news.gmane.org!not-for-mail From: =?utf-8?Q?=C3=93scar_Fuentes?= Newsgroups: gmane.emacs.help Subject: Re: if vs. when vs. and: style question Date: Mon, 30 Mar 2015 03:33:41 +0200 Message-ID: <874mp3clqi.fsf@wanadoo.es> References: <87sicvwckx.fsf@wmi.amu.edu.pl> <87wq27yvqg.fsf@debian.uxu> <8d531e99-7260-4263-ac99-09c6871e2708@googlegroups.com> <87vbhq53lf.fsf@debian.uxu> <87a8z23p23.fsf@kuiper.lan.informatimago.com> <87lhilx0cf.fsf@debian.uxu> <87twx9360u.fsf@kuiper.lan.informatimago.com> <0d1d19ab-06e9-462d-8867-9a49b1e232d3@googlegroups.com> <87pp7x2jav.fsf@kuiper.lan.informatimago.com> <87d23s4nt4.fsf@debian.uxu> <7e8ddf8f-163a-4d16-9ce2-25b0cb3f35aa@googlegroups.com> <87sicny7zm.fsf@kuiper.lan.informatimago.com> NNTP-Posting-Host: plane.gmane.org Mime-Version: 1.0 Content-Type: text/plain; charset=utf-8 Content-Transfer-Encoding: 8bit X-Trace: ger.gmane.org 1427679267 24876 80.91.229.3 (30 Mar 2015 01:34:27 GMT) X-Complaints-To: usenet@ger.gmane.org NNTP-Posting-Date: Mon, 30 Mar 2015 01:34:27 +0000 (UTC) To: help-gnu-emacs@gnu.org Original-X-From: help-gnu-emacs-bounces+geh-help-gnu-emacs=m.gmane.org@gnu.org Mon Mar 30 03:34:17 2015 Return-path: Envelope-to: geh-help-gnu-emacs@m.gmane.org Original-Received: from lists.gnu.org ([208.118.235.17]) by plane.gmane.org with esmtp (Exim 4.69) (envelope-from ) id 1YcOak-0005Ou-Jr for geh-help-gnu-emacs@m.gmane.org; Mon, 30 Mar 2015 03:34:14 +0200 Original-Received: from localhost ([::1]:58888 helo=lists.gnu.org) by lists.gnu.org with esmtp (Exim 4.71) (envelope-from ) id 1YcOaj-0006PP-Sk for geh-help-gnu-emacs@m.gmane.org; Sun, 29 Mar 2015 21:34:13 -0400 Original-Received: from eggs.gnu.org ([2001:4830:134:3::10]:37079) by lists.gnu.org with esmtp (Exim 4.71) (envelope-from ) id 1YcOaZ-0006PK-A3 for help-gnu-emacs@gnu.org; Sun, 29 Mar 2015 21:34:04 -0400 Original-Received: from Debian-exim by eggs.gnu.org with spam-scanned (Exim 4.71) (envelope-from ) id 1YcOaW-00070Y-45 for help-gnu-emacs@gnu.org; Sun, 29 Mar 2015 21:34:03 -0400 Original-Received: from plane.gmane.org ([80.91.229.3]:34387) by eggs.gnu.org with esmtp (Exim 4.71) (envelope-from ) id 1YcOaV-00070M-UQ for help-gnu-emacs@gnu.org; Sun, 29 Mar 2015 21:34:00 -0400 Original-Received: from list by plane.gmane.org with local (Exim 4.69) (envelope-from ) id 1YcOaS-00059J-6h for help-gnu-emacs@gnu.org; Mon, 30 Mar 2015 03:33:56 +0200 Original-Received: from 171.red-80-26-206.adsl.dynamic.ccgg.telefonica.net ([80.26.206.171]) by main.gmane.org with esmtp (Gmexim 0.1 (Debian)) id 1AlnuQ-0007hv-00 for ; Mon, 30 Mar 2015 03:33:56 +0200 Original-Received: from ofv by 171.red-80-26-206.adsl.dynamic.ccgg.telefonica.net with local (Gmexim 0.1 (Debian)) id 1AlnuQ-0007hv-00 for ; Mon, 30 Mar 2015 03:33:56 +0200 X-Injected-Via-Gmane: http://gmane.org/ Original-Lines: 46 Original-X-Complaints-To: usenet@ger.gmane.org X-Gmane-NNTP-Posting-Host: 171.red-80-26-206.adsl.dynamic.ccgg.telefonica.net User-Agent: Gnus/5.13 (Gnus v5.13) Emacs/25.0.50 (gnu/linux) Cancel-Lock: sha1:bYevjGt0toTJnQU/hpkJrxlNUF4= X-detected-operating-system: by eggs.gnu.org: Genre and OS details not recognized. X-Received-From: 80.91.229.3 X-BeenThere: help-gnu-emacs@gnu.org X-Mailman-Version: 2.1.14 Precedence: list List-Id: Users list for the GNU Emacs text editor List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , Errors-To: help-gnu-emacs-bounces+geh-help-gnu-emacs=m.gmane.org@gnu.org Original-Sender: help-gnu-emacs-bounces+geh-help-gnu-emacs=m.gmane.org@gnu.org Xref: news.gmane.org gmane.emacs.help:103431 Archived-At: Stefan Monnier writes: >> 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. Math textbooks teaching the same matter usually start with a table of symbols, with subtle and capricious differences from one book to another. :-) > 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. Those conventions make sense when you work on the same field for long enough periods (students, specialized programmers...) but I guess that most of us deal with heterogeneous code on a regular basis. Heck, we do use different programming languages on the same session. After the end of the day (or week) when you worked on code dealing with finance, graphics, databases, concurrency, the Emacs redisplay, generic algorithms (sorting, etc) and what-not, then you do realize how counterproductive is to rely on non-obvious local conventions. As for the higher concision, it is acceptable for cases where the "read-time"/"think-time" ratio is low (say 15 minutes thinking for each minute reading) but for the common "what this code does" case, where such ratios are unnaceptable and a sign of bad coding, those funny symbols just add cognitive strain.