0 - GiacomoZheng/gm GitHub Wiki

点击前往中文部分

two-part form

"definition" + "statement"

Any language, no matter a natural one or a synthetic one, needs to allowed people to "define" something, even if it is just used temporarily. After all, we cannot always use the old words only.

By the way, the part not the definition are named "statement", so that I call the form as two-part form.

Different language use different ways to differ the "definition" and "statement", but indeed there is only two ways (as I know),

  1. Format: Use different formats for these two part, and
  2. Order: Regard the part with some word shows up at first time as definition.

For most of the natural languages (in fact I only know the Chinese and English), they choose the second way -- order. In addition, the new-defined words is a temporary (I'll talk about details later).

For most of the synthetic languages, at least for the programming languages (I've learnt Python, R, java and Racket), they need to obey both the first and second rules. In other word, you need to use the special format to define a word at the first place it appears. The results of the definitions depends on languages.

In gm, I purely choose the first rule, which means you can use the word before and make up the definition later. For the constants, the order is always meaningless, but for the temporaries, things will be much more complex, I'll explain it later.

Altough gm permit to write without order, I recommend you to write defintions front, if it is possible, at least write the definitions nearby.

Rule of gm is that, all the definition part should contain a : (you can overwrite this symbol later, but now, just follow me), as

@gm.h.s,
a: = 2, ; this sentence is a definition
a = 2 ; this sentence is a statement
■

The : is defined under the location gm (I'll talk about it later), you can use it anywhere.

REMARK: the defining symbol is : but not the :=..

three-part form

"definition", "condition" and "conclusion"

It is possible to express everything purely with the two-part form, but sometimes we may need to use a huge block of definitions, like, (I'm sorry that the markdown and github do not support the syntax highlight of gm now)

@gm.h.Group,
∀G: ∈ group, ∀H: ∈ group,
∀f:
(
	∈ homomorphism,
	f.D = G, f.C = H,
	ker(f) = {G.e}
),
; the above ones are definition

f ∈ injection ; statement
■

we can see that the definition of f is much more longer than G or H.

Here I introduce one more form, I named it as three-part form, in which the statements are divided into two parts, "condition" and "conclusion".

Just like the definition, gm also use format to differ the condition and conclusion. gm use the symbol to separate them. The statements before it are condition, and the ones behind it are the conclusion.

Therefore, the example above can be written as,

@gm.h.Group,
∀G: ∈ group, ∀H: ∈ group,
∀f: ∈ homomorphism,
; above ones are the definition

∀(f.D = G, f.C = H) ⇒ ; two condition
(
	ker(f) = {G.e} ; one more condition
	⇒ f ∈ injection ; conclusion
)
■

Just ignore the other symbols.

These two form can be transformed to each other without loss. In fact, the compiler (I'll write it ...) would translate all the condition into definition.

The is defined under the location gm (the same as :), you can use it anywhere.

Home | Page Down


双段论

“定义” + “陈述”

任何语言,无论是自然语言还是人工语言,都需要允许人们“定义”某些东西,即使它只是暂时使用。毕竟,我们不能总是只使用旧有词。

此外,不是定义的部分被称为“陈述”,所以我将这种格式称为双段论。

不同的语言使用不同的方法来区别“定义”和“陈述”,但归根到底有两种方法(据我所知),

  1. 格式:这两部分使用不同的格式。
  2. 顺序:以某词汇第一次出现的部分为定义。

对于大多数自然语言(事实上我只懂中文和英文),他们会选择第二种方式——顺序。另外,新定义的单词是一个时量(我将在后面讨论细节)。

对于大多数人工语言,至少编程语言(我学习过PythonRjavaRacket),它们需要同时遵守第一和第二规则。换句话说,你需要使用特殊的格式来定义第一个出现的单词。定义的结果取决于语言设定。

gm中,我只使用第一个规则,这意味着你可以在先调用这个词,然后再补上定义。对于常量来说,顺序是没有意义的,但是对于临时量来说,情况有点复杂,我稍后会解释它。

虽然gm允许你书写时无视顺序,但我建议是,如果可能的话,把定义写在前面,不然,至少要写在附近。

gm的规则是,所有的定义部分都应该包含一个:(以后你学会如何重写它,但现在请照做),例如

a: = 2, ; 这句话是定义
a = 2, ; 这句话是陈述

:是在位置gm(我稍后会讲到它)下定义的,你可以在任何地方使用它。

注意:定义符号是:,而不是:=

三段论

“定义” + “条件” + “结论”

我们可以只用双段论书写一切,但有时这么做可能会需要一大块的定义,比如,(很抱歉,markdown和github现在暂不支持gm的语法高亮)

@gm.h.Group,
∀G: ∈ group, ∀H: ∈ group,
∀f:
(
	∈ homomorphism,
	f.D = G, f.C = H,
	ker(f) = {G.e}
),
; the above ones are definition

f ∈ injection ; statement
■

(这是用英语写的,但gm理论上可以全程使用中文)

我们可以看到,f的定义比GH要长得多。

这里我再介绍一种格式,我把它命名为三段式,它把陈述分为两部分,“条件”和“结论”。

就像定义一样,gm也使用格式来区分条件和结论。gm使用来分隔两者。在陈述中,前面的是条件,后面的是结论。因此,上面的例子可以写成,

@gm.h.Group,
∀G: ∈ group, ∀H: ∈ group,
∀f: ∈ homomorphism,
; above ones are the definition

∀(f.D = G, f.C = H) ⇒ ; two condition
(
	ker(f) = {G.e} ; one more condition
	⇒ f ∈ injection ; conclusion
)
■

这两种形式可以毫无损失地相互转化。实际上,编译器(我以后编写它的...)会将所有条件转换为定义。

是在位置gm(与:一样)下定义的,你可以在任何地方使用它。

下页

返回顶部