직관 론적 유형 이론과 동등한 조합 논리는 무엇입니까?

직관 론적 유형 이론과 동등한 조합 논리는 무엇입니까?

---

나는 최근에 Haskell과 Agda (종속 형 함수형 프로그래밍 언어)를 특징으로하는 대학 과정을 마쳤고, 이것들에서 람다 미적분을 조합 논리로 대체 할 수 있는지 궁금했습니다. Haskell을 사용하면 S 및 K 결합자를 사용하여 가능해 보이므로 점이 없습니다. Agda와 동등한 것이 무엇인지 궁금합니다. 즉, 변수를 사용하지 않고 Agda와 동등한 종속 유형의 함수 프로그래밍 언어를 만들 수 있습니까?

또한 정량화를 결합 자로 대체 할 수 있습니까? 이것이 우연인지는 모르겠지만 보편적 인 정량화는 예를 들어 형식 서명을 람다 식처럼 보이게 만듭니다. 의미를 변경하지 않고 형식 서명에서 범용 수량화를 제거하는 방법이 있습니까? 예 :

forall a : Int -> a < 0 -> a + a < a

forall을 사용하지 않고 같은 것을 표현할 수 있습니까?

---

그래서 조금 더 생각하고 진전을 이루었습니다. Martin-Löf의 유쾌하고 단순하지만 일관성이없는 Set : Set시스템을 결합 스타일 로 인코딩하는 첫 번째 방법 입니다. 끝내기에 좋은 방법은 아니지만 시작하기 가장 쉬운 곳입니다. 이 유형 이론의 구문은 유형 주석, Pi 유형 및 유니버스 세트가있는 람다 미적분입니다.

목표 유형 이론

완전성을 위해 규칙을 제시하겠습니다. 컨텍스트 유효성은 Sets에 서식하는 새로운 변수를 인접하여 빈 상태에서 컨텍스트를 구축 할 수 있다고 말합니다 .

                     G |- valid   G |- S : Set
--------------     ----------------------------- x fresh for G
  . |- valid         G, x:S |- valid

이제 우리는 주어진 문맥에서 용어에 대한 유형을 합성하는 방법과 포함 된 용어의 계산 동작까지 어떤 유형을 변경하는 방법을 말할 수 있습니다.

  G |- valid             G |- S : Set   G |- T : Pi S \ x:S -> Set
------------------     ---------------------------------------------
  G |- Set : Set         G |- Pi S T : Set

  G |- S : Set   G, x:S |- t : T x         G |- f : Pi S T   G |- s : S
------------------------------------     --------------------------------
  G |- \ x:S -> t : Pi S T                 G |- f s : T s

  G |- valid                  G |- s : S   G |- T : Set
-------------- x:S in G     ----------------------------- S ={beta} T
  G |- x : S                  G |- s : T

원본에서 약간의 변형으로 람다를 유일한 바인딩 연산자로 만들었으므로 Pi의 두 번째 인수는 반환 유형이 입력에 의존하는 방식을 계산하는 함수 여야합니다. 관례에 따라 (예를 들어 Agda에서는하지만 슬프게도 Haskell에서는 아님) 람다의 범위가 가능한 한 오른쪽으로 확장되므로, 고차 연산자의 마지막 인수 일 때 추상화를 괄호로 묶지 않은 채로 둘 수 있습니다. Pi와 함께. Agda 유형 (x : S) -> T은 Pi S \ x:S -> T.

( 여담 람다합니다. 유형 주석 당신이 할 수 있도록하려면 필요한 합성 추상화의 유형을. 당신이 입력 전환하면 확인 당신의 작업 방식으로, 당신은 여전히 같은 베타 - REDEX을 확인하기 위해 주석을 필요 (\ x -> t) s당신이 방법이 없기 때문에, 전체에서 부품의 유형을 추측하기 위해 현대 디자이너에게 유형을 확인하고 바로 구문에서 베타 redexes를 제외하도록 조언합니다.)

( Digression .이 시스템은 Set:Set다양한 "거짓말 역설"의 인코딩을 허용하기 때문에 일관성이 없습니다 . Martin-Löf가이 이론을 제안했을 때 Girard는 그에게 일관성없는 시스템 U로 인코딩을 보냈습니다. Hurkens로 인한 후속 패러독스는 다음과 같습니다. 우리가 알고있는 가장 유독 한 구조.)

조합기 구문 및 정규화

어쨌든 우리는 Pi와 Set라는 두 개의 추가 기호가 있으므로 S, K 및 두 개의 추가 기호로 조합 번역을 관리 할 수 ​​있습니다. 나는 우주로 U를 선택하고 제품을 P로 선택했습니다.

이제 유형이 지정되지 않은 조합 구문 (자유 변수 포함)을 정의 할 수 있습니다.

data SKUP = S | K | U | P deriving (Show, Eq)

data Unty a
  = C SKUP
  | Unty a :. Unty a
  | V a
  deriving (Functor, Eq)
infixl 4 :.

a이 구문 에 유형 으로 표현되는 자유 변수를 포함하는 방법을 포함했습니다 . 내 부분에서 반사되는 것 외에도 (이름에 걸 맞는 모든 구문은 return변수 를 포함하고 >>=대체를 수행 하는 무료 모나드 임) 조합 형식에 바인딩하여 용어를 변환하는 과정에서 중간 단계를 나타내는 것이 편리 할 것입니다.

정규화는 다음과 같습니다.

norm :: Unty a -> Unty a
norm (f :. a)  = norm f $. a
norm c         = c

($.) :: Unty a -> Unty a -> Unty a        -- requires first arg in normal form
C S :. f :. a $. g  = f $. g $. (a :. g)  -- S f a g = f g (a g)   share environment
C K :. a $. g       = a                   -- K a g = a             drop environment
n $. g              = n :. norm g         -- guarantees output in normal form
infixl 4 $.

(독자를위한 연습은 정확히 정상적인 형태에 대한 유형을 정의하고 이러한 작업의 유형을 선명하게하는 것입니다.)

유형 이론 표현

We can now define a syntax for our type theory.

data Tm a
  = Var a
  | Lam (Tm a) (Tm (Su a))    -- Lam is the only place where binding happens
  | Tm a :$ Tm a
  | Pi (Tm a) (Tm a)          -- the second arg of Pi is a function computing a Set
  | Set
  deriving (Show, Functor)
infixl 4 :$

data Ze
magic :: Ze -> a
magic x = x `seq` error "Tragic!"

data Su a = Ze | Su a deriving (Show, Functor, Eq)

I use a de Bruijn index representation in the Bellegarde and Hook manner (as popularised by Bird and Paterson). The type Su a has one more element than a, and we use it as the type of free variables under a binder, with Ze as the newly bound variable and Su x being the shifted representation of the old free variable x.

Translating Terms to Combinators

And with that done, we acquire the usual translation, based on bracket abstraction.

tm :: Tm a -> Unty a
tm (Var a)    = V a
tm (Lam _ b)  = bra (tm b)
tm (f :$ a)   = tm f :. tm a
tm (Pi a b)   = C P :. tm a :. tm b
tm Set        = C U

bra :: Unty (Su a) -> Unty a               -- binds a variable, building a function
bra (V Ze)      = C S :. C K :. C K        -- the variable itself yields the identity
bra (V (Su x))  = C K :. V x               -- free variables become constants
bra (C c)       = C K :. C c               -- combinators become constant
bra (f :. a)    = C S :. bra f :. bra a    -- S is exactly lifted application

Typing the Combinators

The translation shows the way we use the combinators, which gives us quite a clue about what their types should be. U and P are just set constructors, so, writing untranslated types and allowing "Agda notation" for Pi, we should have

U : Set
P : (A : Set) -> (B : (a : A) -> Set) -> Set

The K combinator is used to lift a value of some type A to a constant function over some other type G.

  G : Set   A : Set
-------------------------------
  K : (a : A) -> (g : G) -> A

The S combinator is used to lift applications over a type, upon which all of the parts may depend.

  G : Set
  A : (g : G) -> Set
  B : (g : G) -> (a : A g) -> Set
----------------------------------------------------
  S : (f : (g : G) ->    (a : A g) -> B g a   ) ->
      (a : (g : G) ->    A g                  ) ->
           (g : G) ->    B g (a g)

If you look at the type of S, you'll see that it exactly states the contextualised application rule of the type theory, so that's what makes it suitable to reflect the application construct. That's its job!

We then have application only for closed things

  f : Pi A B
  a : A
--------------
  f a : B a

But there's a snag. I've written the types of the combinators in ordinary type theory, not combinatory type theory. Fortunately, I have a machine that will make the translation.

A Combinatory Type System

---------
  U : U

---------------------------------------------------------
  P : PU(S(S(KP)(S(S(KP)(SKK))(S(KK)(KU))))(S(KK)(KU)))

  G : U
  A : U
-----------------------------------------
  K : P[A](S(S(KP)(K[G]))(S(KK)(K[A])))

  G : U
  A : P[G](KU)
  B : P[G](S(S(KP)(S(K[A])(SKK)))(S(KK)(KU)))
--------------------------------------------------------------------------------------
  S : P(P[G](S(S(KP)(S(K[A])(SKK)))(S(S(KS)(S(S(KS)(S(KK)(K[B])))(S(KK)(SKK))))
      (S(S(KS)(KK))(KK)))))(S(S(KP)(S(S(KP)(K[G]))(S(S(KS)(S(KK)(K[A])))
      (S(S(KS)(KK))(KK)))))(S(S(KS)(S(S(KS)(S(KK)(KP)))(S(KK)(K[G]))))
      (S(S(KS)(S(S(KS)(S(KK)(KS)))(S(S(KS)(S(S(KS)(S(KK)(KS)))
      (S(S(KS)(S(KK)(KK)))(S(KK)(K[B])))))(S(S(KS)(S(S(KS)(S(KK)(KS)))(S(KK)(KK))))
      (S(KK)(KK))))))(S(S(KS)(S(S(KS)(S(KK)(KS)))(S(S(KS)(S(KK)(KK)))
      (S(S(KS)(KK))(KK)))))(S(S(KS)(S(S(KS)(S(KK)(KS)))(S(KK)(KK))))(S(KK)(KK)))))))

  M : A   B : U
----------------- A ={norm} B
  M : B

So there you have it, in all its unreadable glory: a combinatory presentation of Set:Set!

There's still a bit of a problem. The syntax of the system gives you no way to guess the G, A and B parameters for S and similarly for K, just from the terms. Correspondingly, we can verify typing derivations algorithmically, but we can't just typecheck combinator terms as we could with the original system. What might work is to require the input to the typechecker to bear type annotations on uses of S and K, effectively recording the derivation. But that's another can of worms...

This is a good place to stop, if you've been keen enough to start. The rest is "behind the scenes" stuff.

Generating the Types of the Combinators

I generated those combinatory types using the bracket abstraction translation from the relevant type theory terms. To show how I did it, and make this post not entirely pointless, let me offer my equipment.

I can write the types of the combinators, fully abstracted over their parameters, as follows. I make use of my handy pil function, which combines Pi and lambda to avoid repeating the domain type, and rather helpfully allows me to use Haskell's function space to bind variables. Perhaps you can almost read the following!

pTy :: Tm a
pTy = fmap magic $
  pil Set $ \ _A -> pil (pil _A $ \ _ -> Set) $ \ _B -> Set

kTy :: Tm a
kTy = fmap magic $
  pil Set $ \ _G -> pil Set $ \ _A -> pil _A $ \ a -> pil _G $ \ g -> _A

sTy :: Tm a
sTy = fmap magic $
  pil Set $ \ _G ->
  pil (pil _G $ \ g -> Set) $ \ _A ->
  pil (pil _G $ \ g -> pil (_A :$ g) $ \ _ -> Set) $ \ _B ->
  pil (pil _G $ \ g -> pil (_A :$ g) $ \ a -> _B :$ g :$ a) $ \ f ->
  pil (pil _G $ \ g -> _A :$ g) $ \ a ->
  pil _G $ \ g -> _B :$ g :$ (a :$ g)

With these defined, I extracted the relevant open subterms and ran them through the translation.

A de Bruijn Encoding Toolkit

Here's how to build pil. Firstly, I define a class of Finite sets, used for variables. Every such set has a constructor-preserving embedding into the set above, plus a new top element, and you can tell them apart: the embd function tells you if a value is in the image of emb.

class Fin x where
  top :: Su x
  emb :: x -> Su x
  embd :: Su x -> Maybe x

We can, of course, instantiate Fin for Ze and Suc

instance Fin Ze where
  top = Ze              -- Ze is the only, so the highest
  emb = magic
  embd _ = Nothing      -- there was nothing to embed

instance Fin x => Fin (Su x) where
  top = Su top          -- the highest is one higher
  emb Ze     = Ze            -- emb preserves Ze
  emb (Su x) = Su (emb x)    -- and Su
  embd Ze      = Just Ze           -- Ze is definitely embedded
  embd (Su x)  = fmap Su (embd x)  -- otherwise, wait and see

Now I can define less-or-equals, with a weakening operation.

class (Fin x, Fin y) => Le x y where
  wk :: x -> y

The wk function should embed the elements of x as the largest elements of y, so that the extra things in y are smaller, and thus in de Bruijn index terms, bound more locally.

instance Fin y => Le Ze y where
  wk = magic    -- nothing to embed

instance Le x y => Le (Su x) (Su y) where
  wk x = case embd x of
    Nothing  -> top          -- top maps to top
    Just y   -> emb (wk y)   -- embedded gets weakened and embedded

And once you've got that sorted out, a bit of rank-n skullduggery does the rest.

lam :: forall x. Tm x -> ((forall y. Le (Su x) y => Tm y) -> Tm (Su x)) -> Tm x
lam s f = Lam s (f (Var (wk (Ze :: Su x))))
pil :: forall x. Tm x -> ((forall y . Le (Su x) y => Tm y) -> Tm (Su x)) -> Tm x
pil s f = Pi s (lam s f)

The higher-order function doesn't just give you a term representing the variable, it gives you an overloaded thing which becomes the correct representation of the variable in any scope where the variable is visible. That is, the fact that I go to the trouble of distinguishing the different scopes by type gives the Haskell typechecker enough information to compute the shifting required for the translation to de Bruijn representation. Why keep a dog and bark yourself?

---

I guess the "Bracket Abstraction" works also for dependent types under some circumstances. In section 5 of the following paper you find some K and S types:

Outrageous but Meaningful Coincidences
Dependent type-safe syntax and evaluation
Conor McBride, University of Strathclyde, 2010

Converting a lambda expression into a combinatorial expression roughly corresponds to converting a natural deduction proof into a Hilbert style proof.

참고URL : https://stackoverflow.com/questions/11406786/what-is-the-combinatory-logic-equivalent-of-intuitionistic-type-theory