softwaredesign/wiki/sources/EOS-endnotes-formalism.md

---
title: EOS 형식 의미론 — 개념의 수학적 기반
tags: [source, EOS, formalism]
source: Daniel Jackson (2021), Endnotes 43–44, 64
updated: 2026-04-30
---

# EOS 형식 의미론 — 개념의 수학적 기반

> EOS 본문이 직관적 설명에 집중하는 반면, 엔드노트 43–44, 64는 개념의 수학적 의미론을 다룬다. 이 페이지는 그 기술적 보충 내용을 정리한다.

## 개념의 행동 의미론 (Note 44)

### 상태 기계로서의 개념

개념의 행동은 **상태 기계(state machine)**로 형식화된다.

- **상태(State)**: 개념이 기억해야 하는 것의 집합. 집합과 관계(relation)로 표현
- **초기 상태**: 모든 집합·관계가 비어 있는 상태
- **액션**: 전이 관계(transition relation)로 정의됨
- **결정론(determinism)**: 동일한 상태와 인수에 대해 최대 하나의 후속 상태만 존재

### 트레이스와 상태 함수

**트레이스(trace)** = 가능한 액션 인스턴스의 유한 히스토리

```
state: Trace → State
```

상태 함수는 각 트레이스에 그것이 생성하는 상태를 대응시킨다.

```
state(<create(i0), delete(i0)>) = {accessible: {}, trashed: {i0}}
state(<create(i0), delete(i0), empty()>) = {accessible: {}, trashed: {}}
```

> **fig. E.3** (*trash 개념의 부분 상태 기계 다이어그램*): 3개 상태 — 초기 `{accessible:{}, trashed:{}}`, 좌측 `{accessible:{i0}, trashed:{}}`, 우측 `{accessible:{}, trashed:{i0}}`. 전이: `create(i0)` (초기→좌측), `delete(i0)` (좌측→우측, accessible에서 제거·trashed에 추가), `restore(i0)` (우측→좌측, trashed에서 accessible로 복원), `empty()` (우측→초기, trashed 영구 삭제). 동일 상태·입력에 최대 하나의 후속 상태 — 결정론적 상태 기계.

### 전이 관계, 전제조건, 교착 상태

액션 `A` (인수 집합 X)의 의미론:

```
trans(A) ⊆ S × X × S
```

- **전제조건(precondition)**: 액션이 가능한 (s, x) 쌍의 집합
- 전제조건이 성립하지 않으면 액션은 실행 불가
- **교착 상태(deadlock)**: 어떤 상태에서 가능한 액션이 없는 경우 — 설계 결함

### Alloy를 이용한 액션 형식화

```
pred reserve (u: User, r: Resource) {
  r in available
  reservations' = reservations + u -> r
  available' = available - r
}
```

프라임(`'`)은 Electrum 확장의 약식 표기로 액션 후 값을 나타낸다.

## 운영 원칙의 형식화 (Note 43, 44)

### 동적 논리로 표현

기본 형식: `[a]p` = 액션 a 수행 후 술어 p가 항상 성립

복합 액션 연산자:
- `a;b` — 순차 합성
- `a*` — 반복 (0회 이상)
- `a or b` — 선택
- `not a` — a가 아닌 임의 액션

**trash 개념의 운영 원칙:**
```
delete(x) {can restore(x)}
delete(x); restore(x) {x in accessible}
```

**reservation 개념:**
```
reserve(u, r); (not cancel(u, r))* {can use(u, r)}
```

**style 개념:**
```
define(s, f); assign(e1, s); assign(e2, s); define(s, f') {e1.format = e2.format = f'}
```

### 운영 원칙 vs. 유스케이스/유저 스토리

| 구분 | 운영 원칙 | 유스케이스 |
|------|-----------|-----------|
| 역할 | 개념의 본질 설명 | 기능 전체 기술 |
| 범위 | 개별 개념 단위 | 시스템 레벨 |
| 수량 | 핵심 시나리오 1–2개 | 수십~수백 개 |
| 초점 | 왜 이 개념인가 | 무엇을 할 수 있는가 |

## 객체 분류 (Note 44)

### 역할에 의한 분류

| 역할 | 정의 | 예 |
|------|------|-----|
| **자산(asset)** | 고유 가치를 지닌 객체 | 사진, 오디오 트랙, 블로그 포스트, 인증서 |
| **이름(name)** | 다른 객체를 식별·위치시키는 객체 | 이메일 주소, 도메인 이름, 파일 경로 |
| **값(value)** | 다른 객체와의 관계에서만 의미를 갖는 객체 | 숫자 80 (나이, 온도, 조회수…) |

### 가변성(mutability)에 의한 분류

- **불변(immutable)**: 개념 간 통신(동기화) 시 공유되는 객체는 반드시 불변이어야 함
  - 가변 객체가 공유되면 숨겨진 통신 발생 → 앨리어싱 문제
- 개념 내부에서는 가변 객체 해석 가능

### 해석 가능성(interpretability)에 의한 분류

**비해석(uninterpreted)**: 동등성(equality)만 인식 — 타입 변수처럼 동작

**해석(interpreted)**: 객체의 내부 구조나 값을 활용

**순열 불변성(permutation invariance)으로 형식화:**
타입 T가 개념 C에서 비해석적이면, T의 임의 순열 p에 대해 p(t)도 C의 트레이스이고 `state(p(t)) = p(state(t))`.

> **fig. E.4** (*style 개념(좌)과 Gmail label 개념(우)의 관계형 데이터 모델*): 좌: `Element --(assigned)--> Style --(defined)--> Format`, 점선으로 `Element --(format)--> Format` 파생 관계. 우: `Conversation --(messages)--> Message --(labels)--> Label`, 점선으로 `Conversation --(displays)--> Label` 파생 관계. 파생 상태(derived state)는 두 기본 관계의 합성 경로로 정의됨 — 스타일 개념에서 Element의 실제 format은 Style을 거쳐 결정되며, Gmail에서 대화의 레이블은 메시지를 거쳐 집계됨.

## 조합의 의미론 (Note 64)

### 조합 = 트레이스의 인터리빙

개념들의 조합은 개별 개념 트레이스의 **모든 가능한 인터리빙(interleaving)**이다. 동기화는 허용되는 인터리빙을 제한한다.

동기화 형식:
```
sync action1(x)
     action2(e)
```
의미: 모든 트레이스에서 trigger action1의 모든 발생 직후 반드시 response action2가 발생.

### 핵심 정리: 조합은 개념 행동을 보존한다

> "Composing concepts never changes the behavior of any of the constituent concepts."

이것이 개념 이해 가능성의 근거다. 개념은 어떤 맥락에서도 동일하게 행동한다. 위반 시 → 개념 무결성(concept integrity) 위반 (Ch11).

**안전성(safety) vs. 활성성(liveness)**:
- 조합은 안전성 속성은 보존
- 활성성은 제한 가능 (예: access control 개념이 다른 개념의 액션을 억제)

> **fig. E.5** (*Photoshop에서의 layer + mask 개념*): 흑백 사과 이미지 편집 화면. Layers 패널: "Curves 1" 조정 레이어(흰 원 마스크 = 사과 영역만 조정 적용) + "Background" 원본 레이어. 마스크가 Curves 조정을 사과에만 한정 — 원본 픽셀 불변(비파괴 편집). layer 개념 + mask 개념의 시너지 조합: 두 개념 각각의 행동이 조합 후에도 보존되면서 비파괴 로컬 편집이라는 창발적 기능 실현.

### CSP와의 관계

개념 조합의 의미론은 Tony Hoare의 CSP(Communicating Sequential Processes)에서 파생.

차이점:
| | CSP | 개념 조합 |
|--|-----|---------|
| 결정론 | 비결정론적 가능 | 항상 결정론적 |
| 상태 관찰 | 없음 | 동기화 조건에 상태 사용 가능 |
| 동기화 | 공유 액션 | trigger/response 쌍 |

## 생성 입력 (Note 64)

액션의 입력에는 두 종류:
1. **생성 입력(generated input)**: 개념 자체가 생성 — `gen` 키워드로 표시
2. **제공 입력**: 다른 개념이 제공

```
add(gen t: Task)           // task는 todo 개념이 생성
affix(i: Item, gen l: Label)  // item은 외부 제공, label은 label 개념이 생성
```

트레이스 제약: `gen`이 아닌 입력은 트레이스의 이전 액션에서 생성 또는 출력된 것이어야 한다.

## 관련 개념

- [[EOS-ch4-concept-structure]] — 개념의 5요소 (informal)
- [[EOS-ch6-concept-composition]] — 개념 조합 전반
- [[propagation]] — SDF의 전파 모델과 비교 (유사한 수학적 구조)