당신이 지적했듯이, λ- 미적분학은 겉보기 단순 시간 복잡성의 개념을 가지고 있습니다 : 단지 β- 감소 단계의 수를 세십시오. 불행히도 상황은 간단하지 않습니다. 우리는 물어야합니다 :

 Is counting β-reduction steps a good complexity measure?

M

$M$|M|

$|M|$M

$M$poly(|M|)

$poly(|M|)$tr(M)

$tr(M)$poly(|tr(M)|)

$poly(|tr(M)|)$

오랫동안 이것이 λ- 미적분에서 달성 될 수 있는지는 불분명했습니다. 주요 문제는 다음과 같습니다.

• 지수 크기의 다항식 단계로 정규형을 생성하는 항이 있습니다. (1)을 참조하십시오. 정상적인 형태를 쓰더라도 지수 시간이 걸립니다.

• 선택한 축소 전략도 중요한 역할을합니다. 예를 들어, 다항식 수의 병렬 β- 단계 (최적의 λ- 감소 (2)의 의미에서, 그러나 복잡성은 비 원소 (3, 4)) 인 용어 군이 존재합니다.

이 백서 (1)는 가장 왼쪽에있는 Call-By-Name 감소를 가정 하여 복잡성 클래스 PTIME 을 보존하는 합리적인 인코딩을 보여줌으로써 문제를 명확히합니다 . 중요한 통찰력은 지수 폭발이 하위 용어를 적절히 공유하여 패배 할 수있는 흥미없는 이유에서만 발생할 수 있다는 것 같습니다.

(1)과 같은 논문은 β- 단계 또는 Turing-machine 단계를 계산하든 PTIME 과 같은 복잡한 클래스가 일치 함을 보여줍니다 . 그렇기 때문에 O (log n) 과 같이 복잡도가 낮은 클래스 도 일치 한다는 의미 는 아닙니다. 물론 이러한 복잡성 클래스는 튜링 머신 모델의 변형 (예 : 1- 테이프 대 멀티 테이프)에서도 안정적이지 않습니다.

D. Mazza의 연구 (5)는 튜링 기계 대신 기능 언어 (λ- 미적분의 변형)를 사용하여 쿡 레빈 정리 (SAT의 complete 완전성)를 증명합니다. 핵심 통찰력은 다음과 같습니다.

$$\frac{\text{Boolean circuits}}{\text{Turing machines}}=\frac{\text{affine $\lambda$-terms}}{\text{$\lambda$-terms}}$$

공간 복잡성에 관한 상황이 이해되는지 모르겠습니다.

1. B. Accattoli, U. Dal Lago, 베타 감소는 변하지 않습니다 .

2. 제이 제이 Levy, Reductions는 dans le lambda-calcul을 수정하고 최적화합니다.

3. JL Lawall, HG Mairson, 최적 성과 비 효율성 : 람다 미적분학의 비용 모델이 아닌 것은 무엇 입니까?

4. A. Asperti, H. Mairson,
   병렬 베타 감소는 기본 재귀가 아닙니다 .

5. D. Mazza, 교회는 Cook과 Levin을 만난다 .

답변