Факторальды Kappa-есепте қозғалмайтын нүкте операторымен кодталуы мүмкін бе?

$ $ \ Kappa $ -calculus операторы $ fix $ бар, ол функцияны $ (1 \ rightarrow a) түрімен түрлендіру үшін қолданылуы мүмкін \ rightarrow a $ типі $ 1 түрінде \ rightarrow a $. Біз қалыпты төмендету стратегиясын қолданамыз.

Мұндай жүйеде факторлық функцияны ұсынамыз. Мәселе мынада, кез-келген функция біз тұрақты нүктені табуға тырысамыз, функцияны түзету нүктесіне қолданғанда, $ x $ дәлелінің мәнін немесе қажет емес екенін анықтаудың жолы жоқ. Біздің шешімді негіздеу үшін «қарсы» жоқ.

$ fix (\ kappa {} x. \ cdots) = (\ kappa {} x. \ cdots) (fix (\ kappa {} x. \ cdots)) $

$ \ Lambda $ -calculus ішінде біз $ fix (\ lambda f. \ lambda x. \ Cdots) $ іске қосып, $ x $ мәніне байланысты тоқтатамыз.

  1. Тұрақты нүкте операторымен $ \ kappa $ -calculus фактологиялық функцияны шынымен көрсете алмайтындығын қалай дәлелдеуге болады?
  2. жалпылама көрсеткілер ?
5

1 жауаптар

Жалаңаш $ \ kappa $ -calculus бекітілген нүкте операторымен ұзартылған кезде де формантты анықтауға мүмкіндік бермейді. Дегенмен, бұл жауап кейбір ашуға лайық.

  1. The fixed point operator you give is not well-formed according to the grammar of types in the $\kappa$-calculus. Note that the grammar of types does not contain the function space $\tau \Rightarrow \tau'$ -- this is because the $\kappa$-calculus is a language of first-order functions. An expression has a type $\tau_1 \to \tau_2$, to indicate that it is an expression of type $\tau_2$, whose free variables are typed by $\tau_1$.

    The proper typing for a fixed point operator would be roughly something like: $$ \frac{\Gamma, x:1 \to \tau \vdash e : 1 \to \tau} {\Gamma \vdash \mu x:1 \to \tau. e : 1 \to \tau} $$

  2. Once you've fixed this, you still can't define a factorial.

    The plain $\kappa$-calculus does not have sums or natural numbers as a base type. As a result, you can't write branching programs, and so you cannot define interesting recursive functions. If you added natural numbers and their iterator, you could define a factorial function. Hasegawa actually gives factorial as an example in his paper on the $\kappa$-calculus, in a calculus augmented with a basic natural number type.

    However, you might wonder why you are able to define factorial in the pure lambda calculus, even though it has no apparent control structures. The reason is that the interaction of fixed points and recursion gives you a "universal type" (i.e., a type $V$ such that $V$ is isomorphic to $V \to V$), and this lets you encode any datatype as a subset (more accurately, a retract) of it.

    In more syntactic terms, you can write the Y combinator (i.e., Curry's paradox) in any language with (a) higher-order functions, (b) recursion, and (c) the ability to use each variable more than once in a program. Since the basic $\kappa$-calculus lacks (a), adding even an unrestricted fixed point operator does not make it Turing-complete!

9
қосылды
Ұмытылмаған көрсеткілерді $ + $ типтегі примитивтерді де ұмытпаңыз. Тьюринг аяқтау үшін $ \ kappa $ -calculus жасау үшін қарапайым рекурсия және азайту операторларының бір түрі қажет сияқты. Үлкен жауап үшін рахмет.
қосылды автор William Martins, көзі