1.1基本概念 ·一个简单的例子 (入x:nt.(y:nat.入Z:nmt.(x+y)+Z)3)45 =(入x:nat.Z:nat.(x+3)+Z）45 =(入Z:nmt.(4+3)+Z) =(4+3)+5 =12
1.1 基 本 概 念 • 一个简单的例子 ( x : nat. ( y : nat. z : nat. ( x + y ) + z ) 3 ) 4 5 = ( x : nat. z : nat. ( x + 3 ) + z ) 4 5 = ( z : nat. ( 4 + 3 ) + z ) 5 = ( 4 + 3 ) + 5 = 12
1.1基本概念 ·入表示法中有两个约定 函数应用是左结合的：MNP应看成MN)P 每个入的约束范围尽可能地大： 一直到表达式的结束，或 碰到不能配对的右括号为止 例 -入x:c.MN解释为入x:G.(MN),而不是(x:g.M0N -入x:o.入y:x.MW是入x:c.(2y:x.(MW)的简写 (x:.(y:云.（入z:p.M)W)P)2可以简写为 -0 (入x:o.入：x.入zp.M)NP
1.1 基 本 概 念 • 表示法中有两个约定 – 函数应用是左结合的： MNP 应看成 (MN)P – 每个的约束范围尽可能地大： 一直到表达式的结束，或 碰到不能配对的右括号为止 • 例 – x:.MN解释为x:.(MN)，而不是(x:.M)N – x:.y:.MN是x:.(y:.(MN))的简写 – (((x:.(y:.(z:.M)))N)P)Q可以简写为 (x:.y:.z:.M)NPQ