递归是否仅作用于单个判别参数？关于递归定义与Coq实现的疑问

递归是否只能作用于单个判别参数？ #

那种“递归必须作用于单个判别参数”的说法并不全面。在递归定义里，完全存在多参数同步参与递归的情况——比如自然数减法的标准递归定义（当两个参数都是后继形式时，会同时递归到它们的子项），还有你写的less_than函数，都是这类双参数递归的典型例子。

递归的核心要求是递归调用的参数满足“良基性”（比如自然数的话，参数的大小严格递减），而非限制只能有一个判别参数。

《计算类型论》中否定操作的第三种模式 #

从你提供的定义截图来看，第三种否定模式的形式应为¬(S x, S y) = ¬(x, y)。这里的否定操作确实是作用于对两个参数分别判别（都解构为后继构造子）后得到的变量x和y，而非仅针对第一个参数。这种定义属于双参数同步递归，通过同时拆解两个参数的构造结构，生成递归调用的参数。

你的Coq less_than函数分析 #

看你实现的less_than函数：

Fixpoint less_than (n m : nat) :=
  match n with
  | 0 =>
    match m with
    | 0 => false
    | S y => true
    end
  | S x =>
    match m with
    | 0 => false
    | S y => less_than x y
    end
  end.

在递归调用less_than x y时，x是对第一个参数n（S x形式）解构后得到的子项，y是对第二个参数m（S y形式）解构后得到的子项。也就是说，这个递归调用确实作用于对两个参数判别后得到的变量——只有当n和m都处于S _的构造形式时，才会触发双参数同时递减的递归调用，逻辑和前面提到的减法、否定操作的第三种模式完全一致。

内容的提问来源于stack exchange，提问作者Seeker