请输入您要查询的字词:

 

单词 110PatternMatchingAndRecursion
释义

1.10 Pattern matching and recursion


The natural numbersMathworldPlanetmath introduce an additional subtlety over the types considered up until now.In the case of coproducts, for instance, we could define a function f:A+BC either with the recursor:

f:𝗋𝖾𝖼A+B(C,g0,g1)

or by giving the defining equations:

f(𝗂𝗇𝗅(a)):g0(a)
f(𝗂𝗇𝗋(b)):g1(b).

To go from the former expression of f to the latter, we simply use the computation rules for the recursor.Conversely, given any defining equations

f(𝗂𝗇𝗅(a)):Φ0
f(𝗂𝗇𝗋(b)):Φ1

where Φ0 and Φ1 are expressions that may involve the variablesa and b respectively, we can express these equations equivalently in terms of the recursor by using λ-abstraction:

f:𝗋𝖾𝖼A+B(C,λa.Φ0,λb.Φ1).

In the case of the natural numbers, however, the “defining equations” of a function such as 𝖽𝗈𝗎𝖻𝗅𝖾:

𝖽𝗈𝗎𝖻𝗅𝖾(0):0(1)
𝖽𝗈𝗎𝖻𝗅𝖾(𝗌𝗎𝖼𝖼(n)):𝗌𝗎𝖼𝖼(𝗌𝗎𝖼𝖼(𝖽𝗈𝗎𝖻𝗅𝖾(n)))(2)

involve the function double itself on the right-hand side.However, we would still like to be able to give these equations, rather than (LABEL:eq:dbl-as-rec), as the definition of 𝖽𝗈𝗎𝖻𝗅𝖾, since they are much more convenient and readable.The solution is to read the expression “𝖽𝗈𝗎𝖻𝗅𝖾(n)” on the right-hand side of (2) as standing in for the result of the recursive call, which in a definition of the form 𝖽𝗈𝗎𝖻𝗅𝖾:𝗋𝖾𝖼(,c0,cs) would be the second argument of cs.

More generally, if we have a “definition” of a function f:C such as

f(0):Φ0
f(𝗌𝗎𝖼𝖼(n)):Φs

where Φ0 is an expression of type C, and Φs is an expression of type C which may involve the variable n and also the symbol “f(n)”, we may translate it to a definition

f:𝗋𝖾𝖼(C,Φ0,λn.λr.Φs)

where Φs is obtained from Φs by replacing all occurrences of “f(n)” by the new variable r.

This style of defining functions by recursion (or, more generally, dependent functions by inductionMathworldPlanetmath) is so convenient that we frequently adopt it.It is called definition by pattern matching.Of course, it is very similar to how a computer programmer may define a recursive functionMathworldPlanetmath with a body that literally contains recursive calls to itself.However, unlike the programmer, we are restricted in what sort of recursive calls we can make: in order for such a definition to be re-expressible using the recursion principle, the function f being defined can only appear in the body of f(𝗌𝗎𝖼𝖼(n)) as part of the composite symbol “f(n)”.Otherwise, we could write nonsense functions such as

f(0):0
f(𝗌𝗎𝖼𝖼(n)):f(𝗌𝗎𝖼𝖼(𝗌𝗎𝖼𝖼(n))).

If a programmer wrote such a function, it would simply call itself forever on any positive input, going into an infinite loop and never returning a value.In mathematics, however, to be worthy of the name, a function must always associate a unique output value to every input value, so this would be unacceptable.

This point will be even more important when we introduce more complicated inductive types in http://planetmath.org/node/87578Chapter 5,http://planetmath.org/node/87579Chapter 6,http://planetmath.org/node/87585Chapter 11.Whenever we introduce a new kind of inductive definition, we always begin by deriving its induction principle.Only then do we introduce an appropriate sort of “pattern matching” which can be justified as a shorthand for the induction principle.

随便看

 

数学辞典收录了18232条数学词条,基本涵盖了常用数学知识及数学英语单词词组的翻译及用法,是数学学习的有利工具。

 

Copyright © 2000-2023 Newdu.com.com All Rights Reserved
更新时间:2025/5/4 22:38:08