O cálculo SK2 é uma base completa, onde K2 é o combinador K invertido?

10

Especificamente, se eu definisse um novo K2 como

K2=λx.(λy.y)
vez de
K=λx.(λy.x)
o {S,K2,I} -calculus ser uma base competir?

Meu palpite é "não", apenas porque parece que não consigo construir o combinador K regular a partir de S , I e K2 combinadores, mas eu não tenho um algoritmo de seguir, nem tenho boa intuição sobre como fazer coisas com esses combinadores.

Parece que você pode definir

K2=KI
com o cálculo regular {S,K,(I)} , mas eu realmente não consegui trabalhar para trás para obter uma derivação de K em termos de K2 e o resto .

Minha tentativa de provar que ela não estava funcionalmente completa tentou essencialmente construir exaustivamente todas as funções possíveis desses combinadores, a fim de mostrar que você alcança um beco sem saída (uma função que você já viu antes), independentemente dos combinadores que você usa. Sei que isso não é necessariamente verdade para conjuntos de combinadores funcionalmente incompletos (por exemplo, o combinador K por si só nunca terá um beco sem saída quando aplicado a si mesmo), mas esse foi o meu melhor pensamento. Eu sempre fui capaz de usar o combinador S para escapar do que eu pensava ser finalmente um beco sem saída, então não tenho mais tanta certeza da viabilidade dessa abordagem.

Eu fiz esta pergunta no StackOverflow mas fui encorajado a publicá-la aqui. Recebi alguns comentários sobre esse post, mas não tenho certeza se os entendi direito.

Bônus: se não for uma base completa, o idioma resultante ainda é Turing completo?

Cole
fonte
Este é um belo quebra-cabeça. Parece que S e K 'apenas permitem gerar termos cujas formas normais da cabeça têm até três λs iniciais (ou seja, termos que normalizam com a forma λx₁.λx₂.λx₃. Xᵢ t₁ ... tₙ), de modo que pode ser outro caminho para provar a incompletude, embora pareça um pouco complicado de formalizar. Definitivamente, você nunca chega a um "beco sem saída": comece definindo I = λx.x = K2 K2, depois repetindo a transformação t ↦ S t K2, você pode expressar λx.x I ... I para qualquer sequência de Is .
Noam Zeilberger
... E desculpe, por "incompletude", quero dizer a incompletude de SK 'como base combinatória para o cálculo lambda não tipado. Também não tenho uma boa intuição sobre se é ou não Turing-completo (o que seria implícito na completude combinatória, mas não o contrário).
Noam Zeilberger
Postagens cruzadas : stackoverflow.com/q/55148283/781723 , cs.stackexchange.com/q/108741/755 . Por favor, não postar a mesma pergunta em vários sites . Cada comunidade deve ter uma chance honesta de responder sem perder tempo com ninguém.
DW
Meu erro, @DW, há algo que eu possa fazer para remediar isso?
cole

Respostas:

14

Considere os termos do cálculo S,K2,I como árvores (com nós binários representando aplicativos e folhas S,K2 representando os combinadores.

Por exemplo, o termo S(SS)K2 seria representado pela árvore

        @
       / \
      /   \
     @    K2
    / \
   /   \
  S     @
       / \
      /   \
     S     S

T@K2

S,K2,I

         @                           @
        / \                         / \
       /   \                       /   \
      @     g    [reduces to]     @     @
     / \                         / \   / \
    /   \                       e   g f   g
   @     f                 
  / \
 /   \
S     e
      @
     / \
    /   \
   @     f    [reduces to]   f
  / \
 /   \
K2    e

TTTTTS,K2,ITK2SK2KK2SK2KS,K2,I

ZAK
fonte
Muito bom argumento!
Noam Zeilberger
Argumento muito liso e claro. Obrigado. Talvez eu abra uma pergunta separada para perguntar sobre a integridade de Turing.
cole
5

S,K2,I


A,B,C

  • K:ABA
  • K2:ABB
  • S:(ABC)(AB)(AC)
  • I:AA

KI,S,K2ABB,(ABC)(AB)(AC),AAAABBABA

t,f,uABB(ABC)(AB)(AC)AAt

A B | A -> B
t t | t
t f | f
f t | t
f f | t
t u | f
f u | t
u t | t
u f | f
u u | t

K2,S,IttABAfuAtBS,K2,I

ZAK
fonte
11
Eu gosto da abordagem, mas você poderia esclarecer quais regras você está adotando como seu cálculo sequencial?
Noam Zeilberger
Você pode esboçar como provar S neste cálculo seqüencial restrito? Não parece ser possível com as regras que eu imaginei que você quis dizer.
Robin Houston
11
@ robin-houston: veja minha edição (também adicionei um argumento semântico diferente com a mesma conclusão).
ZAK
2
Concordo com Charles Stewart (aqui: twitter.com/txtpf/status/1123962607306706944 ) de que não está claro como passar da desabitada no cálculo lambda de tipo simples para a inexprimibilidade usando combinadores. Pode haver um argumento específico para K, mas a etapa inicial "... então também se pode fazer a mesma coisa no cálculo-λ de tipo simples" não se aplica em geral (Charles mencionou o contra-exemplo do combinador Y) . Você vê como tornar esse argumento rigoroso?
Noam Zeilberger
11
K