람다 미적분학을 배우고 있습니다. 그러나 나는 람다 미적분학의 한정어에 대해 매우 혼란스러워합니다. 내가 아는 한, "∃"와 같은 양화어는 λ 계산법에 필요하지 않은 1 차 논리 (FOL)의 개념입니다. 게다가, 내가 읽은 튜토리얼에서 수량 한정어에 관해서 아무 것도 발견하지 못했다.람다 미적분학의 한정어
하지만, I는 this paper 찾을 저자 람다 계산법의 정량을 사용하는 첫 번째 페이지 (람다 성분 의미 의존성 기준). 그렇다면 람다 미적분학에서 사용되는 수량 기호는 무엇입니까? 그렇다면 무엇을 의미합니까? FOL과 같은가요?
당신이 인용 한 종이는 술어를 사용하는 것과 같은 방식으로 수량 적으로 다소 비공식적으로 사용하고 있습니다. 이미 람다 (lambda) 미적분학을 가지고 있다면 적어도 종이에서 FOL의 한정 기호를 포함하여 원하는 정식 기호 세트로 그것을 확장 할 수 있습니다. 이 경우 한정 기호는 미적분에 추가되는 것이지 일부는 아닙니다.
한정자는 으로 입력 할 수 있습니다. 단, 람다 미적분을 입력 할 수 있습니다. 간단히 입력 된 설정에서는 기본 함수 유형이 있지만 범용 한정 기호 및 dependent function/Pi types으로 일반화 할 수 있습니다. 이 경우 람다 식은 함축적 인 의미와 보편적 인 양을 의미합니다. 즉, 람다 식에 부여 할 수있는 의미 해석을 기반으로합니다. 그런 다음 존재 한정어를 다음과 같이 정의 할 수 있습니다.
∃ : t. P a : = ∀Q. (∀a : t. P a → Q) → Q
일반 제품 유형과 동일한 데이터입니다.