78651d5da1
- EOS-endnotes-formalism: 개념의 수학적 의미론 (상태기계·트레이스·조합·CSP·동적 논리) - EOS-endnotes-context: 역사·철학·비교 맥락 (Parnas·DDD·Alloy·기입 이론·오버로딩 분류) - concepts-181-328 (엔드노트+참고문헌+인덱스) 전량 컴파일 완료 Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>
176 lines
5.9 KiB
Markdown
176 lines
5.9 KiB
Markdown
---
|
||
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: {}}
|
||
```
|
||
|
||
### 전이 관계, 전제조건, 교착 상태
|
||
|
||
액션 `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))`.
|
||
|
||
## 조합의 의미론 (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 개념이 다른 개념의 액션을 억제)
|
||
|
||
### 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의 전파 모델과 비교 (유사한 수학적 구조)
|