In this paper, we propose a computational interpretation of the generalized Kreisel-Putnam rule, also known as the generalized Harrop rule or simply the Split rule, in the style of BHK semantics. We will achieve this by exploiting the Curry-Howard correspondence between formulas and types. First, we inspect the inferential behavior of the Split rule in the setting of a natural deduction system for the intuitionistic propositional logic. This will guide our process of formulating an appropriate program that would capture the corresponding computational content of the typed Split rule. In other words, we want to find an appropriate selector function for the Split rule by considering its typed variant. Our investigation can also be reframed as an effort to answer the following questions: is the Split rule constructively valid in the sense of BHK semantics? Our answer is positive for the Split rule as well as for its newly proposed generalized version called the S rule.

翻译：本文基于BHK语义，对广义Kreisel-Putnam规则（亦称广义Harrop规则或简称为Split规则）提出了一种计算解释。我们将通过利用公式与类型之间的Curry-Howard对应来实现这一目标。首先，在直觉主义命题逻辑的自然演绎系统框架中，考察Split规则的推理行为。这将指导我们设计适当的程序，以捕获带类型的Split规则对应的计算内容。换言之，我们希望通过考虑其带类型变体，为Split规则找到合适的择函数。我们的研究也可重新表述为回答以下问题的尝试：Split规则在BHK语义意义上是否具有构造有效性？我们的答案是肯定的，对于Split规则及其新提出的广义版本——S规则均成立。