关于类型((a -> c) -> c) -> a的全终止函数可实现性咨询

Great question! Let's unpack this clearly, starting with definitions and then diving into the type signature you're curious about.

Yes, your intuition is spot-on. A total terminating function has two non-negotiable properties:

• It's total: it’s defined for every possible input in its domain—no gaps, no undefined cases, no errors.
• It's terminating: for every input, it finishes computing in a finite number of steps. No infinite loops, no infinite recursion, no "stuck" states where it can’t produce a valid result.

In short: it always gives you a valid output, and it never runs forever.

The answer hinges on the type system or logical framework you’re working with—this is a classic example tied to the Curry-Howard isomorphism, where types correspond to logical propositions and functions correspond to proofs.

In intuitionistic systems (e.g., pure λ-calculus, Haskell’s pure subset, Coq without classical axioms) #

No, such a function does not exist.

Here’s the breakdown:
The type ((a -> c) -> c) -> a maps to the logical proposition ((A → C) → C) → A. In intuitionistic logic, this is equivalent to double negation elimination (if you set C = False, it becomes ¬¬A → A). Intuitionistic logic rejects this as an axiom because it doesn’t align with constructive reasoning: just because "it’s not true that A is false" doesn’t mean "A is true" (think of undecidable statements like "there are infinitely many twin primes"—we can’t construct a proof of the statement itself, but we can say it’s not provably false).

To formalize this proof:

1. Use the Curry-Howard isomorphism to translate the type into its corresponding logical proposition.
2. Show the proposition isn’t intuitionistically valid (e.g., via a Kripke model where ¬¬A holds but A does not).
3. Since intuitionistic type systems only "inhabit" types that correspond to provable propositions, this type has no total terminating functions here.

Note: You can write a function with this type in non-total systems (like Haskell) that loops infinitely (e.g., badDne f = f (\x -> badDne f)), but this isn’t terminating, so it doesn’t count as a valid total terminating function.

In classical systems (e.g., logic with the law of excluded middle, Coq with classical axioms) #

Yes, such a function exists.

Classical logic accepts the law of excluded middle (LEM: forall a. Either a (a -> Void)—every statement is either true or false), which lets us construct a total terminating function for this type. Here’s how it might look in a Haskell-like syntax (using LEM as an axiom):

-- Assume the law of excluded middle as a valid classical axiom
excludedMiddle :: forall a. Either a (a -> Void)
excludedMiddle = undefined -- In a classical system, this is a legitimate axiom

absurd :: Void -> c
absurd v = case v of {} -- No cases to handle, so this is total and terminating

dne :: ((a -> c) -> c) -> a
dne f = case excludedMiddle @a of
  Left x -> x -- We have a direct value of a, return it
  Right notA -> f (\x -> absurd (notA x)) -- Use f to derive a from its negation

This function is total (covers all inputs via LEM) and terminating (both branches finish in finite steps—absurd is trivially terminating, and f is assumed to be a total terminating input).

Proving non-existence (intuitionistic systems) #

• Curry-Howard Isomorphism: Map the type to a logical proposition, then show the proposition isn’t provable in intuitionistic logic (e.g., via Kripke semantics or proof-theoretic arguments).
• Normalization Theorems: For systems like System F (second-order λ-calculus), all closed terms normalize (terminate). If the type had an inhabitant, it would lead to a contradiction (e.g., constructing a term that can’t normalize, or violating parametricity).

Proving existence (classical systems) #

• Curry-Howard Isomorphism: Show the proposition ((A → C) → C) → A is a classical tautology (using truth tables or natural deduction with LEM/double negation elimination).
• Construct the Function: Build an explicit λ-term using classical axioms (like LEM) and verify it’s total and terminating—every branch must finish in finite steps, and all inputs are covered.

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