aboutsummaryrefslogtreecommitdiffstats
path: root/docs
diff options
context:
space:
mode:
Diffstat (limited to 'docs')
-rw-r--r--docs/design/029-past-one-node.md18
1 files changed, 11 insertions, 7 deletions
diff --git a/docs/design/029-past-one-node.md b/docs/design/029-past-one-node.md
index a7f4966..5f2c7bb 100644
--- a/docs/design/029-past-one-node.md
+++ b/docs/design/029-past-one-node.md
@@ -144,7 +144,7 @@ C의 속도로 컴파일하기 쉬운 쪽**이어야 한다. 61–183배의 절�
| exact | 메모리의 칸과 부름의 기계를 지움. double과 검사, FLAT `PureList`(append마다 `list_held`와 `grows`), `Text`의 복사, 트리의 `ranges`, 예산은 남김 | 8,785 | 4,002 | 3.02 | 오늘 증명됨: 스택의 모양과 타입, fn마다의 등록기·리스트·바꾸는 집합 |
| integer | 정수를 정수로 | 7,979 | 3,547 | 1.10 | **N1** 정수임(새로) |
| stored_flat | `ranges`의 열을 평평하게 | 6,561 | 2,800 | 1.22 | **N2** 처리기의 바꾸는 집합(있는 분석을 처리기로 넓힘) |
- | local_flat | 사건의 리스트, 점, `out`을 타입 있는 버퍼로(append마다 메모리 셈은 남김) | 696 | 364 | 9.43 | **N3** let 리스트가 받는 연산(덧붙이기, 자리 읽기, 세기뿐: 키 없음, 인덱스 상태 없음)(새). 원소 타입은 정적이고, 정수 열은 N1 |
+ | local_flat | 사건의 리스트, 점, `out`을 타입 있는 버퍼로(append마다 메모리 셈은 남김) | 696 | 364 | 9.43 | 오늘의 선언: 사건의 리스트이고 키도 인덱스 상태도 없다(`state_key`, `state_indexed`). 원소 타입은 정적이고, 정수 열은 N1. 새 사실이 아니라 표현의 결정이다 |
| shared | `Text`가 버퍼를 함께 씀(복사 없음) | 564 | 317 | 1.23 | **N4** 담은 뒤 바뀌지 않음: `LIST_VALUE` 뒤에 그 리스트도 레코드의 리스트도 바뀌지 않는다(새) |
| unbounded | 경계 검사를 지움 | 502 | 298 | 1.12 | (N5 경계 안임: 막대에 필요 없어 넣지 않음) |
| plain | 예산과 메모리 셈까지 지움: 같은 알고리즘의 C | 362 | 258 | 1.39 | 셈은 계약이라 증명으로 지우지 않는다 |
@@ -159,11 +159,15 @@ C의 속도로 컴파일하기 쉬운 쪽**이어야 한다. 61–183배의 절�
- **전제 하나를 고친다.** let 리스트는 영속 트리가 아니다. 실행기는 사건의 리스트를 처음부터 FLAT 배열로 둔다(021, `pure_list_arrays`:
담은 것에 맞춰 폭을 고르는 열). 9.43배는 트리가 아니라 범용 리스트의 길에서 온다. append마다 `pure_list_insert`의 폭 고르기와
넓히기, `list_held`가 앞뒤로 부르는 함수 여덟, 읽기마다 꼴과 폭의 갈래와 double로의 바꿈이 든다. 트리는 저장 리스트 `ranges`뿐이다.
- - **새로 증명할 사실은 셋, 넓힐 분석은 하나다(N1–N4).** 오늘의 증명(스택의 모양과 타입, fn마다의 등록기·리스트·바꾸는 집합)이 exact를
- 허락한다. 이 앱의 fn 여섯은 제 사건 리스트가 없고 아무것도 바꾸지 않으며, 등록기는 부름마다 제 것이라 C의 지역이 된다. 그 위에
- N1 정수임, N3 let 리스트의 연산, N4 담은 뒤 바뀌지 않음은 새로 증명해야 하고, N2는 fn에 하는 분석을 처리기로 넓히면 된다. 확인한 것:
- 입력 리스트는 aup가 바꾸지 못하게 한다(언어의 뜻이라 증명이 필요 없다). 담은 뒤 바꾸는 것은 aup가 허락하므로 N4는 지점마다
- 증명해야 한다.
+ - **새로 증명할 사실은 둘, 넓힐 분석은 하나다(N1, N4, N2).** 오늘의 증명(스택의 모양과 타입, fn마다의 등록기·리스트·바꾸는 집합)이
+ exact를 허락한다. 이 앱의 fn 일곱(range와 여섯)은 제 사건 리스트가 없고 아무것도 바꾸지 않으며, 등록기는 부름마다 제 것이라 C의
+ 지역이 된다. 그 위에 N1 정수임과 N4 담은 뒤 바뀌지 않음은 새로 증명해야 하고, N2는 fn에 하는 분석을 처리기로 넓히면 된다.
+ - 가장 큰 인자(9.43배)는 새 사실이 필요 없다. 키가 없고 인덱스 상태도 없는 사건의 리스트가 받는 연산(덧붙이기, 넣기, 빼기, 읽기,
+ 쓰기, 세기, 찾기, 접기, 걷기)은 타입 있는 버퍼가 모두 한다. 키와 인덱스는 모듈에 선언되어 있고, 사건의 리스트임은 구조로 안다.
+ 필요한 것은 표현의 결정(021의 폭을 고르는 FLAT 배열과 범용 API 대신 타입 있는 버퍼)과 메모리 셈의 계약이다.
+ - 처음 이 자리(커밋 `7ffb114`)에 "새로 셋"이라 적으며 N3(let 리스트가 받는 연산)을 넣었다. 그것은 오늘의 선언이 이미 든 것이라 뺐다.
+ - 확인한 것: 입력 리스트는 aup가 바꾸지 못하게 한다(언어의 뜻이라 증명이 필요 없다). 담은 뒤 바꾸는 것은 aup가 허락하므로 N4는
+ 지점마다 증명해야 한다.
- 단서.
- exact는 소스에서 썼다. C의 `&&`와 `||`는 필요한 데까지만 가고, 읽기마다의 `LIST_BIND`는 없으며, cc가 fn을 인라인할 수 있다. 그래서
exact는 충실한 내보내기보다 싸다. 이어 붙임 → exact의 인자는 크게, exact 뒤의 인자들은 작게 나왔을 수 있다.
@@ -177,7 +181,7 @@ C의 속도로 컴파일하기 쉬운 쪽**이어야 한다. 61–183배의 절�
- **고친 것: 막대의 셈.** "명령 하나가 기계 명령 하나여도 C의 2.5배"라고 적었다. 명령의 수가 바닥이라고 본 것인데, range()의 both는
실행된 명령 269.5개를 기계 명령 226개로 한다(하나에 0.84). 레지스터 아래에서 옮김과 상수가 사라진다. 그 셈은 틀렸다.
- **원리 1이 지금 말하는 것.** 시험한 길(실행기의 몸을 이어 붙이기)은 죽었다(앱 1.43배, range() 1.78배). 표현까지 포함해 증명에서
- 내보내는 것은 UAX #14의 처리기에서 C의 2.5배(사이클 3.6배)다. 새 사실 셋과 넓힌 분석 하나가 필요하고, 계약(검사와 셈)과 알고리즘이
+ 내보내는 것은 UAX #14의 처리기에서 C의 2.5배(사이클 3.6배)다. 새 사실 둘과 넓힌 분석 하나가 필요하고, 계약(검사와 셈)과 알고리즘이
남는다. 사건 자체(1,566)는 이 길 밖이다. 손으로 쓴 점 하나이지, 지은 내보내기가 아니다.
## 원리 2. 커밋이 곧 복제본이다