Skip to content

Posts 내가 나의 할아버지일 수 있을까 #
Find similar titles

I'm My Own Grandpa라는 노래가 있다고 한다. 내가 나 스스로의 할아버지라는 뜻인데, 이게 어떻게 가능할까?

Alloy Analyzer #

MIT에서 개발한 Alloy Analyzer라는 소프트웨어가 있다. 문법에 맞춰 논리 구조를 기술하고, 해당 논리가 성립할 경우 일어나야 하는 일과 일어나지 않아야 하는 일을 기술하면 1) 일어나야 하는 일이 실제로 일어나는지(사례), 2) 일어나지 않아야 하는 일이 일어나지 않는지(반례) 찾아주는 소프트웨어이다.

이 소프트웨어를 이용하여 정말 내가 나 스스로의 할아버지가 될 수 있는지 알아보자. 참고로 아래 내용은 Software Abstractions: Logic, Language, and Analysis 4장의 내용 일부를 요약/해설한 것이다.

사람, 남자, 여자, 엄마, 아빠 #

일단 할아버지에 대해 정의해야 한다. 그러기 위해서는 가족 관계에 대한 몇 가지 용어들, 그들 사이의 관계를 먼저 정의할 필요가 있다.

우선 사람, 남자 사람, 여자 사람, 엄마, 아빠:

abstract sig 사람 {
    아빠: lone 남자,
    엄마: lone 여자
}
sig 남자 extends 사람 {}
sig 여자 extends 사람 {}

짧은 코드이지만 설명이 좀 필요하다:

  • sig 사람사람이라는 이름의 집합을 정의한다.
  • 남자 extends 사람남자라는 집합을 정의하되, 이 집합이 사람의 부분집합임을 명시한다. 또 동일한 집합을 extends한 집합들은 서로소(disjoint)이다. 남자이면서 동시에 여자인 경우는 없다는 뜻이다. 달리 말하면 남자와 여자의 교집합은 공집합이라는 뜻.
  • 한편, 사람 집합을 선언하는 부분을 보면 그냥 sig가 아니라 abstract sig라고 되어 있는데, 이는 남자도 아니고 여자도 아닌 사람은 존재하지 않음을 뜻한다. 달리 말하면 남자와 여자의 합집합은 사람 전체와 같다는 뜻.
  • 사람에 대한 선언 안에는 아빠엄마가 정의되어 있다. 이는 관계대수의 relation 개념에 해당하는데 아빠라는 relation은 사람에서 남자로 향하는 대응관계를 정의한다. lone이라는 키워드는 0개 혹은 1개를 뜻한다. 즉 모든 사람은 0명 혹은 1명의 아빠, 0명 혹은 1명의 엄마를 갖는다는 뜻이다.

부부 #

이제 부부 개념을 추가하자. 아래와 같이 남자여자에 관계를 추가해주면 된다:

sig 남자 extends 사람 {
    아내: lone 여자
}
sig 여자 extends 사람 {
    남편: lone 남자
}

남자 사람은 0명 혹은 1명의 여자 사람과 "아내" 관계에 있고, 여자 사람은 0명 혹은 1명의 남자 사람과 "남편" 관계에 있다.

("남자 사람", "여자 사람"이라는 표현이 뭔가... 대단히 논리적으로 사고하는 느낌을 주지 않나? 그야말로 병신같지만 멋있다 ㅋㅋ)

팩트들 #

이제 할아버지에 대해 정의하면 되나? 아직 아니다. 몇 가지 제약을 더 추가해야 한다:

fact 부부관계 {
    아내 = ~남편
}

부연을 해보면:

  • fact란 주어진 사실로 간주되어야 하는 제약들을 뜻한다. 사례 혹은 반례를 찾을 때 fact에 위배되는 조합은 고려하지 말아야 한다는 뜻이다.
  • ~ 기호는 전치(transpose)를 뜻하고 = 기호는 동치 관계를 뜻한다. 이몽룡이 성춘향의 남편이면 성춘향은 이몽룡의 아내이어야 한다는 뜻이다.

팩트를 하나 더 추가해보자:

fact 생물학적_사실 {
    no p: 사람 | p in p.^(엄마+아빠)
}

일단 전체 뜻은 "내가 나의 조상일 수는 없다"는 생물학적 사실을 나타내는데, 이상한 기호가 왕창 나왔으니 역시나 부연이 필요할 것 같다:

  • no p: 사람 | 어쩌고 저쩌고: "어쩌고 저쩌고"에 해당하는 사람 p는 존재하지 않는다
  • (엄마+아빠): 엄마와 아빠의 합집합. 즉 엄빠.
  • .: 관계대수의 join. 사실 여기에 좀 더 심오한 내용이 담겨 있지만 생략(원소와 집합과 관계를 동일하게 취급한다거나, join이 일어날 때 좌측 relation의 오른쪽 칼럼과 우측 relation의 왼쪽 칼럼이 사라진다거나)
  • ^: Transitive closure. 쉽게 말해서 "엄빠+엄빠의 엄빠+엄빠의 엄빠의 엄빠..."를 모두 포괄하는 집합.
  • in: 포함 관계.
  • 따라서 전체 문장은 "자신(p)의 엄빠+엄빠의 엄빠+엄빠의 엄빠의 엄빠...(.^) 집합에 자기 자신이 속해있는(in) 그러한 사람 p(p: 사람)는 존재하지 않는다(no)"라는 뜻.

드디어, 할아버지란? #

할아버지는 엄마의 아빠(외할아버지) 혹은 아빠의 아빠(친할아버지)를 뜻한다. 이에 대한 함수를 만들어주자:

fun 할아버지 [p: 사람]: set 사람 {
    let 엄빠 = 아빠 + 엄마 |
        p.엄빠.엄빠 & 남자
}

1) 엄빠를 아빠와 엄마의 합집합으로 정의하고, 2) 엄빠의 엄빠 중 남자인 사람을 골라내는 식으로 표현했다.

이제 드디어 실행을 할 차례. "내가 내 할아버지이다"에 해당하는 술어(predicate)를 정의하고 이 술어가 참이 되는 사례를 보여달라고 요청(run)하면 된다.

pred 내가_내_할아버지 [p: 사람] {
    p in p.할아버지
}

run 내가_내_할아버지 for 5

위 코드에서는 runfor 5에 대해서만 설명하면 될 것 같다. 위에서 온갖 집합을 정의하였는데, 각각에 대하여 원소가 최대 5개 이하인 공간을 몽땅 뒤져서(!) 보여달라는 의미이다.

실행을 하면:

No instance found. Predicate may be inconsistent.

라고 나온다. "내가 내 할아버지이다"라는 술어에 해당하는 사례를 찾지 못했고, 이 술어는 논리적으로 비일관적인 것 같다 뜻이다.

일관적이면 일관적이고 아니면 아니지 "인 것 같다"는 뭔 소리인가? 모든 조합을 뒤진 것이 아니라 각 집합의 원소가 5개 이하인 경우에 대해서만 찾아봤기 때문이다. 탐색 공간을 더 넓히면 사례가 발견될지도 모른다는 뜻.

할아버지의 재정의 #

아니 그럼 유행가에서 뻥을 친건가? 양부모를 포함하는 개념으로 할아버지를 좀 더 넓게 정의해보자. 현재 할아버지는 아래와 같이 정의되어 있는데:

fun 할아버지 [p: 사람]: set 사람 {
    let 엄빠 = 아빠 + 엄마 |
        p.엄빠.엄빠 & 남자
}

이를 아래와 같이 고치자:

fun 할아버지 [p: 사람] : set 사람 {
    let 엄빠 = 아빠 + 엄마 + 아빠.아내 + 엄마.남편 |
        p.엄빠.엄빠 & 남자
}

이를테면 내 친엄마의 아빠가 아니더라도, 아빠의 아내(양엄마)의 아빠이면 할아버지로 치자는 뜻이다.

이렇게 고치고 다시 실행을 하면:

Instance found. Predicate is consistent.

라고 나온다. 사례가 발견되었고 술어는 우리가 정의한 논리와 일관성이 있다는 뜻이다. 이번에는 아까처럼 애매하게 "인 것 같다"고 하지 않고 단정적으로 표현하고 있다. 말 그대로 사례를 찾았기 때문이다.

사례가 발견되면 이를 다이어그램으로 보여주는 기능이 있다. 온갖 사례들이 있지만 가장 단순한 것은 아래와 같다:

Image

남자1호(...)가 그 주인공인데, 아빠의 엄마, 즉 자신의 할머니와 결혼을 하는 막장짓을 하여 자기가 자기 스스로의 할아버지가 됐다.

막장짓 금지 #

아무리 세상이 막 돌아가도 이래서야 되겠나. 막장짓을 금지하는 제약을 주어진 사실(fact)로 추가해주자:

fact 직계조상과_결혼_금지 {
    no (아내 + 남편) & ^(엄마 + 아빠)
}

부부 지간이면서 동시에 직계 조상인 그런 관계는 존재할 수 없다는 선언이다.

다시 실행을 해보면? 여전히 사례가 발견된다. 이번에 발견된 사례는 이런 식:

Image

이번에도 남자1호가 주인공. 아빠의 아내의 엄마, 즉 새엄마의 엄마랑 결혼을 했다. 이것도 비슷한 수준의 막장짓이지만 적어도 근친혼은 아니다. 또 다른 사례:

Image

해석은 각자...;;

전체 코드 #

abstract sig 사람 {
    엄마: lone 여자,
    아빠: lone 남자
}

sig 남자 extends 사람 {
    아내: lone 여자
}
sig 여자 extends 사람 {
    남편: lone 남자
}

fact 생물학적_사실 {
    no p: 사람 | p in p.^(엄마+아빠)
}

fact 부부 {
    아내 = ~남편
}

fact 직계조삭과_결혼_금지 {
    no (아내 + 남편) & ^(엄마 + 아빠)
}

fun 할아버지 [p: 사람] : set 사람 {
    let 엄빠 = 아빠 + 엄마 + 아빠.아내 + 엄마.남편 |
        p.엄빠.엄빠 & 남자
}

pred 내가_내_할아버지 [p: 사람] {
    p in p.할아버지
}

run 내가_내_할아버지 for 5

실제 가사는? #

실제 노래 가사의 주인공은 어쩌다가 스스로의 할아버지가 되었을까? 아래 동영상을 참고하자:

그래서 이걸 어디에 쓰나 #

주로 소프트웨어를 더 잘 설계하기 위해 개발자나 설계자가 쓴다고 한다. 나는 기획자들이 이런 도구를 익혀서 쓰면 정말 좋겠다고 생각한다. 사실 Alloy Analyzer는 NDC 2011에서 간단히 소개한 바 있다. 대충 이런 맥락이었다:

  • 개발자들은 정적 문법 검사기, 자동화된 테스트 등 온갖 좋은 도구를 쓴다. 기획자에게도 엑셀이나 파워포인트 이외의, 기획을 도와주는 도구가 필요하다. NetLogo, Alloy Analyzer 등을 적극적으로 발굴해서 익히자.
  • 맹목적인 측정과 A-B testing은 과학적 방법론의 일부일 뿐이다. 현상을 기술(describe)하는 것을 넘어서서 설명(explain)하고 예측(predict)하려면 발견한 사실들을 일반화하여 재활용 가능한 모델로 만들고 축적하기 위해 노력을 해야한다.

난 이런 공부를 하는 기획자들이 많아지면 좋겠다.

Suggested Pages #

Other Posts #

0.0.1_20140628_0