확장적 테일러 전개

우리는 확장적 리소스 항 계산을 소개한다. 이는 에르하르트-레그니에의 리소스 항과 유사하지만 무한히 η-긴 형태이다. 이 계산은 여전히 유한한 구문과 역학을 유지한다: 특히 우리는 강한 수렴성과 정규화를 증명한다. 그 다음 우리는 확장적 테일러 전개의 정의를 내린다. 이는 일반적인 λ-항을 (가능적으로 무한한) 확장적 리소스 항의 선형 조합으로 매핑한다: 일반적인 경우와 마찬가지로, 우리의 리소스 계산의 역학을 통해 λ-항의 β-환원을 시뮬레이션할 수 있다; 이 확장적 전개의 특성은 우리가 η-환원도 시뮬레이션할 수 있다는 것이다. 어떤 의미에서, 확장적 리소스 항은 나카지마 트리의 유한 근사물에 대한 언어를 포함한다. 일반적인 리소스 항이 유한 뵘 트리의 더 풍부한 버전으로 간주될 수 있는 것과 마찬가지이다. 우리는 확장적 테일러 전개의 정규화에 의해 유도되는 동치 관계가 H∗, 가장 일관되고 감각적인 λ-이론 - 나카지마 트리에 의해 유도되는 이론과도 같다는 것을 보여준다. 이 특성화는 확장적 리소스 계산을 모델링하는 것만으로도 H∗의 모델을 제공할 수 있음을 보여준다. 확장적 리소스 계산은 또한 타입화된 설정에 국한되었던 테일러 전개와 게임 의미론 사이의 연결을 타입 없는 설정에서 회복할 수 있게 해준다. 실제로, 단순 타입화된, η-긴, β-정규 리소스 항은 멜리에스의 호모토피 동치까지 하이랜드-옹 게임 의미론의 플레이와 일대일 대응이 된다는 것이 알려져 있다. 확장적 리소스 항은 타입 없는 설정에서 η-긴 리소스 항의 적절한 대응물이다: 우리는 정규 확장적 리소스 항과 증강(호모토피 동치까지의 정준 표현)의 동형 클래스 사이의 대응을 설명한다.