타입이 지정되지 않은 효과(Untyped Effects)를 위한 다범주적 의미론 (Multicategorical Semantics)

범주론적 의미론 (Categorical semantics)에서의 완전성 증명 (Completeness proofs)은 대개 합성이 치환 (Substitution)에 의해 주어지는 구문적 범주 (Syntactic category)를 구축함으로써 진행됩니다. 타입이 지정되지 않은 효과적 Call-by-Value 언어의 경우, 평가 순서 (Evaluation order)가 의미론적으로 중요하기 때문에 계산 (Computation)의 동시 치환에 대한 정형화된 개념이 없다는 근본적인 장애물에 부딪힙니다. 우리는 단일 계산 치환, 즉 바인딩 단계 (Binding steps)를 원시적인 것으로 취하고, 계산 치환을 연결 (Concatenation)로 구성된 유한한 순차적 리스트로 표현함으로써 이 문제를 해결합니다. 우리는 이 아이디어를 하나의 객체를 가진 Freyd-multicategorical 설정에서 정형화합니다. 우리는 Freyd operad를 도입하여, 값 (Values)의 카테시안 operad (Cartesian operad)와 계산 (Computations)의 대칭적 Ren-cartesian preoperad (Symmetric Ren-cartesian preoperad)를 분리하고, 이들을 Freyd functor로 연결하며, 임의의 Freyd operad로부터 그에 대응하는 치환의 Freyd PROP을 구축합니다. 우리는 이 구축이 표현 가능하며 (Representable), 엄격한 하나의 객체 설정에서는 공역 1로의 제한 (Restriction to codomain 1)에 대한 좌수반 (Left adjoint)임을 증명합니다. 유도된 항 모델 (Term model)을 사용하여, 우리는 절차 (Procedures)와 고차 함수 (Higher-order functions)를 가진 타입이 지정되지 않은 계산적 람다 계산법 (Computational lambda-calculus)을 약하게 닫힌 (Weakly closed) Freyd operad에서 해석하고, 건전성 (Soundness), 초기성 (Initiality), 그리고 완전성 (Completeness)을 증명합니다. 이는 타입이 지정되지 않은 효과적 계산에 맞춤화되어 있으며, 모나딕 조합 대수 (Monadic combinatory algebras)와 같은 실현 가능성 지향 모델 (Realizability-oriented models)을 포괄할 수 있을 만큼 충분히 광범위한 범주론적 의미론을 제공합니다.