Loading [MathJax]/jax/output/HTML-CSS/jax.js

ABOUT ME

한 컴퓨터공학과 학생이 개인 공부 용도로 운영하는 블로그입니다.

Today
Yesterday
Total
  • [프언] #03. Inductive Definitions
    2023-2학기/프로그래밍언어 2023. 9. 9. 15:47

    Inductive Specification

    이번 글에서는 Induction에 대해 알아볼 것입니다. Induction은 어떤 값들의 모임, 즉 집합을 정의하기 위해서 사용되는 아주 강력한 도구 중 하나입니다.  예시로 설명드리겠습니다.

    자연수 n이 아래 조건 중 하나를 만족하면 nS라고 합시다.

    1. n=0
    2. n3S

    일단 확실하게 알 수 있는 건 0S의 원소입니다. 그리고 2번 조건에 의해 33S의 원소이므로 3 역시 S의 원소이겠죠? 같은 방법으로 6,9,12,.. 이렇게 3의 배수들은 전무 S의 원소라는 사실을 직관을 통해 알 수 있습니다. 이런 방식으로 집합을 정의하는 것을 Induction이라고 합니다.

    S={0,3,6,9,...}={x|x=3k,kN}

    이에 대한 면밀한 증명은 수학적 귀납법(Mathematical Induction)으로 가능하지만 어렵지 않기도 하고 중요하지도 않아서 따로 하지 않겠습니다.

    위에서 정의한 집합 S와 같은 집합을 Inductive 하게 정의하는 방법에는 정말 여러 가지가 있습니다.

    아래 조건 중 하나를 만족하는 가장 작은 자연수 집합 T은 집합 S와 동일합니다.

    1. 0T
    2. if nS, then n+3T

    '가장 작은'이라는 수식어가 추가로 붙은 이유는 이 수식어가 없으면 {0,1,3,4,6,7,9,10,12,13,..}과 같은 집합도 아래 조건을 만족하기 때문입니다.

    이런 식으로 두 정의 모두 0에서 시작하여 3의 배수를 집합에 포함시키는 것은 동일하지만 약간의 차이가 있습니다. 집합 S와 같은 정의 방식을 Top-down definition, 집합 T와 같은 정의 방식을 Bottom-up definition이라고 부릅니다.

     

    Rule of Inference

    여기에서 한 가지 표현에 대한 정의를 할 건데요. 어떤 논리식을 기반으로 새로운 논리식을 만드는 과정을 우리는 Inference(추론)라고 부릅니다.

    AB

    이 표현은 "if A, then B"를 나타내는 표현이고 이 자체를 Inference Rule이라고 부릅니다. A가 참이면, B도 참이다.라는 뜻이죠. 이때 A를 Hypothesis(전제) 혹은 Antecedent, B를 Conclusion(결론) 혹은 Consequent라고 부릅니다.

    B

    이 Inference Rule은 전제가 없고 결론만 있는데요. 항상 성립한다는 뜻이겠죠? 이렇게 특별한 증명 없이 항상 참이라고 받아들여질 수 있는 명제를 Axiom(공리)이라고 부릅니다.

    그리고 Inference Rule에서 전제는 1개가 아닐 수도 있습니다.

    ABC

    이렇게 적게 되면 이 Inference Rule은 "if A and B, then C"를 의미합니다.

     

    Examples of Inference Rule

    이제 이렇게 새로운 표현을 사용해서, 위에 정의했던 집합 S을 다시 정의해 보겠습니다.

    0SnS(n+3)S

    아까 집합 S를 정의할 때는 위 조건을 만족하는 "가장 작은 집합"이라는 말이 붙어있었는데요, Inference Rule을 사용하면 굳이 "가장 작은 집합"이라는 말이 필요가 없습니다. Inference Rule 표현 자체가 이미 가장 작은 집합이라는 뜻을 내포하고 있기 때문입니다.

    또 다른 예시로, 알파벳 {a,b,c,d,...,z}으로 만들 수 있는 string의 집합 U를 한번 정의해 보겠습니다. 이해를 돕기 위해 집합 U의 대략적인 모습을 적어드리자면 {a,b,...,z,aa,ab,...,az,ba,bb,...}와 같은 모습입니다. Inference Rule로 한번 표현해 보면 아래와 같습니다.

    εαaααbα...αzα

    (여기서 ε은 빈 String을 의미합니다.) 이렇게 빈 String에서 시작하여 알파벳을 하나하나 쌓아나가는 방식으로 집합 U를 정의할 수 있습니다. 조금 더 간단하게 정리하면 아래와 같겠죠.

    x{a,b,...,z},εαxα

    다음 예시로는 실수로 이루어진 List의 집합을 한번 정의해 보겠습니다.

    nillnl(nZ)

    (역시 nil은 빈 List를 의미합니다.) 이렇게 정의된 집합은 실수로 이루어진 모든 List를 포함합니다. 그 예시로 329라는 List가 이 집합에 포함된다는 사실을 한번 증명해 보겠습니다.

    먼저 정의로부터 아래라고 적을 수 있습니다.

    nil9nil(9Z)

    그리고, 9nil이 집합의 원소이므로, 아래라고 적을 수 있습니다.

    9nil29nil(2Z)

    이렇게 2개의 Inference Rule을 이용해 29nil이 집합의 원소라는 사실을 보일 수 있었는데요, 이 2개의 Inference Rule을 하나로 합쳐서 적을 수 있습니다.

    nil9nil(9Z)29nil(2Z)

    이제 마지막으로 한 단계만 더 적어주면 329가 이 집합에 포함된다는 사실을 증명할 수 있겠죠?

    nil9nil(9Z)29nil(2Z)329nil(3Z)

    이렇게 Inference Rule을 연속적으로 적어 논리 전개 과정을 표현한 것을 Derivation Tree 혹은 Deduction Tree라 부릅니다.

    마지막으로 조금 더 복잡한 예시를 한번 보겠습니다. 더하기, 빼기, 곱하기, 괄호로 이루어진 정수 연산식의 집합을 한번 정의해 볼 건데요, 이것도 이때까지의 예시와 똑같이 Inductive 하게 정의할 수 있습니다. 아래 Inference Rule을 한번 보겠습니다.

    nnZeee1e2e1+e2e1e2e1×e2e(e)

    아까처럼 1×(2+3)이 집합에 속한다는 사실을 Derivation Tree를 이용해 증명해 보겠습니다.

    수식으로 보면 조금 복잡해 보일 수 있겠지만 차근차근 생각해 보면 크게 어렵지 않습니다.

     

    Scala에서의 Inductive Data Type

    우리는 프로그래밍을 할 때 Inductive 하게 정의된 Data Type을 자주 사용하게 됩니다. 이런 Data Type을 구현하기 위해서 보통 TraitCase Class를 사용합니다. 예시로 아까 봤던 List의 집합을 Scala에서 한번 구현해 보겠습니다.

    sealed trait IntList
    case Class Nil() extends IntList
    case Class Cons(h: Int, t: IntList) extends IntList
    
    val n = Nil()
    val l = Cons(10, Cons(9, Nil()))
    println(n.isInstanceOf[IntList])	// true
    println(n.isInstanceOf[Nil])		// true
    println(n.isInstanceOf[Cons])		// false
    println(l)				// Cons(10, Cons(9, Nil()))

    갑자기 못 보던 문법들이 훅 등장했는데, 저도 완벽하게 이해를 한 건 아니지만 제가 이해한 선에서 최대한 설명해 보도록 하겠습니다. (Scala에 관련된 인터넷 글들이 전부 자바를 기반으로 작성되어 있는데, 저는 자바에 익숙하지 않아서 이해하는데 시간이 너무 오래 걸렸습니다..)

    클래스끼리는 서로 상속 관계가 존재합니다. 이에 대해 간단히 설명해 보겠습니다. "사람"이라는 클래스가 있고 이 클래스를 상속받는 "학생", "직장인", "백수"등의 클래스가 있다고 생각하면, "사람"이라는 클래스에 존재하는 여러 속성들(성별, 주민등록번호, 출생 국가 등이 있겠죠)을 "학생", "직장인" 클래스에서도 사용할 수 있게 됩니다. 이때 "사람"이라는 클래스를 부모 클래스, "학생", "직장인", "백수"등의 클래스를 자식 클래스라고 부릅니다.

    자바에서는 기본적으로 하나의 클래스가 여러 클래스의 자식이 될 수 없습니다. 우리는 이를 다중 상속이라고 부르는데요. 물론 여러 클래스를 상속받을 수 있다면 좋긴 합니다. 다양한 클래스에 존재하는 다양한 속성들과 메소드들을 사용할 수 있기 때문이죠. 하지만 다중 상속은 여러 가지 문제점을 발생시킬 수 있기 때문에, 자바에서는 다중 상속을 지원하지 않습니다. (어떤 문제점인지는 저도 잘 모르기도 하고 중요하지도 않아서 패스하겠습니다.)

    하지만 다중 상속의 장점을 버릴 수는 없기에, 자바에서는 Class 대신 Interface라는 것을 이용하면 다중 상속을 사용할 수 있습니다. 이 Interface 역할을 하는 것이 Scala의 Trait입니다.

    이제 위의 코드를 한번 다시 봅시다. Trait로 정의된 IntList가 존재하고, 그 밑에는 Case Class로 정의된 Nil과 Cons가 존재합니다. (Case Class에 대한 설명은 이 전 글을 참고해 주세요.) 그리고 Nil과 Cons를 정의할 때, "extends IntList"라는 부분이 있는데요, 이 부분이 바로 Nil과 Cons가 IntList를 상속받는다는 의미입니다. 이때, IntList는 Nil과 Cons의 Supertype, Nil과 Cons는 IntList의 Subtype이라고 부릅니다.

    그러면 여기서, IntList가 여러 클래스를 상속받는 게 아닌데, 위에 내용은 왜 설명한 거냐?라는 질문이 생기실 수 있습니다. 그런데 이건 사실 저도 잘 모르겠습니다.. 왜 굳이 Trait를 사용했는지는요. 아마 나중의 확장성을 위해 그랬을 것이라는 추측이 들기는 하는데 일단 여기서는 넘어가는 걸로 하겠습니다.

     

    이제 위 코드의 Semantics에 대해 조금 알아보겠습니다. 먼저 Nil은 말 그대로 빈 리스트를 의미합니다. 그리고 Cons는 Int 하나와 IntList 하나를 받는 클래스로, 받은 IntList에 받은 Int를 넣어주는 기능을 합니다.

    "Cons(9, Nil())"은 빈 리스트에 9를 추가한, [9]를 의미하겠죠. "Cons(10, Cons(9, Nil()))"같은 경우는 [9]에 10을 추가한 [9, 10]이 되는 것입니다. 이렇게 아까 설명했던 것처럼, 빈 리스트에서 원소들을 하나하나 추가하면서 리스트를 구축해 나가는 것이기 때문에 이를 Inductive 하게 정의되는 Data Type이라고 부르는 것입니다.

    그 아랫부분의 코드는 읽어보시면 무슨 의미인지 쉽게 이해할 수 있을 것입니다. isInstanceOf는 이 오브젝트가 이 Type의 멤버인지 확인하는 기능을 합니다. n은 Nil로 정의되었기 때문에 Nil의 멤버이고, Nil은 IntList의 Subtype이므로 n은 IntList의 멤버이기도 합니다. 따라서 n.isInstanceOf[IntList]와 n.isInstanceOf[Nil]은 True가 되는 것이고, n.isInstanceOf[Cons]는 False가 되겠죠.

     

    이제 IntList 하나를 받아 이 IntList에 존재하는 모든 원소의 합을 출력하는 메소드를 하나 만들어보겠습니다.

    def sum(l: IntList): Int = {
    	if (l.isInstanceOf[Cons]) {
    		val c = l.asInstanceOf[Cons]
    		c.h + sum(c.t)
    	}
    	else
    		0
    }
    
    println(sum(Cons(1, Cons(2, Cons(3, Nil())))))
    // prints 6

    먼저 if가 하나 보이죠. 먼저 else 쪽을 보자면, 받은 IntList가 Cons의 멤버가 아니라는 것은 받은 IntList가 빈 리스트라는 의미이므로 0이 이 함수의 계산값이 됩니다.

    이제 IntList가 Cons의 멤버일 경우에 존재하는 코드 두줄을 한번 봅시다. 먼저 asInstanceOf는 이 값을 이 Type의 오브젝트로 바꿔주는 역할을 합니다. "l.asInstanceOf[Cons]"는 l의 Type을 Cons로 바꾸어주는 역할을 합니다. Cons는 가장 마지막에 리스트에 추가되는 원소 h와, 그 나머지 리스트인 t로 이루어져 있기 때문에, "val c = l.asInstanceOf[Cons]"은 받은 IntList를 가장 마지막 원소와 그 외의 부분으로 분리시켜 주는 코드라고 생각하시면 되겠습니다.

    그러면 c.h는 받은 IntList의 마지막 원소, c.t는 그 외의 부분이 되기 때문에, "c.h + sum(c.t)"가 Inductive 하게 정의된 받은 IntList의 모든 원소의 합이 됩니다. (Cons 클래스의 속성에 대해서는 바로 위에 있는 코드블록이 아닌 그 위에 있는 코드블록을 참고해 주세요.)

     

    많은 프로그래밍 언어에서 Pattern Matching을 지원하는데, Scala 역시 마찬가지입니다. 위의 코드도 Pattern Matching을 이용하면 더 간단하게 작성 가능합니다.

    def sum(l : IntList): Int = l match {
    	case Cons(h, t) => h + sum(t)
    	case Nil() => 0
    }

    감사합니다.


    이 글은 컴퓨터공학과 학부생이 개인 공부 목적으로 작성한 글이므로, 부정확하거나 틀린 내용이 있을 수 있으니 참고용으로만 봐주시면 좋겠습니다. 레퍼런스 및 글에 대한 기본적인 정보는 이 글을 참고해 주세요.

    '2023-2학기 > 프로그래밍언어' 카테고리의 다른 글

Designed by Tistory.