consider the natural numbers defined by the following BNF
m,n::=Z｜S(n)
and the function add defined inductively as follows:
add(Z,m)= m
add(S(n),m)=S(add(n,m))
(1)compute add(S(S(Z)),S(Z));
(2)prove that Z is the left unit of add, i.e., add(n,Z)=n for all natural numbers n;
(3)prove by induction that Z is the right unit of add, i.e., add(Z,n)=n for all natural numbers n;
(4)prove by induction that add(n,S(m))=S(add(n,m)) for all natural numbers n and m;
(5)prove by induction that add is associative.

真想帮你，可是不认识英格兰文字。你能解释一下题目啥意思吗？

有些名词我不知道怎么翻译，就是先根据BNF范式定义了自然数（第一个式子），之后又定义了一个应用add,第一问就是计算add(),第二问是求证明Z是add的左单元（left unit）即，对于所有自然数n有add(Z,n)=n；第三问是求归纳证明Z是add的右单元（right unit）即，对于所有自然数n有add(n,Z)=n；第四问是对于所有自然数n和m有那个式子成立。第五问是归纳证明add是关联的（associative）.

这玩意太难  看百度百科 也不知道是啥玩意

巴科斯范式 以美国人巴科斯(Backus)和丹麦人诺尔(Naur)的名字命名的一种形式化的语法表示方法，用来描述语法的一种形式体系，是一种典型的元语言。又称巴科斯-诺尔形式(Backus-Naur form)。它不仅能严格地表示语法规则，而且所描述的语法是与上下文无关的。它具有语法简单，表示明确，便于语法分析和编译的特点。BNF表示语法规则的方式为：非终结符用尖括号括起。每条规则的左部是一个非终结符，右部是由非终结符和终结符组成的一个符号串，中间一般以“：：=”分开。具有相同左部的规则可以共用一个左部，各右部之间以直竖“|”隔开