람다 미적분학의 정식 설명을 읽을 때, 변수 세트는 항상 무한대로 정의되는 것으로 보입니다. 이 세트가 유한 할 수없는 이유는 분명합니다. 변수 세트를 유한으로 정의하면 용인 될 수없는 방식으로 용어 구조가 제한됩니다. 그러나 세트가 무한대로 무한하게 허용하지 않는 이유는 무엇입니까?람다 미적분학의 변수 집합이 일반적으로 무한 계산 가능으로 정의되는 이유는 무엇입니까?
현재 내가받은이 질문에 대한 가장 분별있는 대답은 셀 수없이 무한한 변수 집합을 선택하면 자연스러운 알파 재 작성을 위해 신선한 변수를 선택하는 방법을 설명하는 변수를 열거 할 수 있음을 의미합니다.
이 질문에 대한 명확한 답변을 찾고 있습니다.
이 집합을 계산할 필요가있는 이유는 매우 간단합니다. 변수가 가득 찬 가방을 가지고 있다고 상상해보십시오. 세트가 부인할 수 없다면이 가방의 변수 수를 세는 방법은 없습니다.
가방은 자루와 동형입니다.
수학과 논리의 대부분의 정의와 구조에는 원하는 결과를 얻기 위해 필요한 최소한의 장치 만 포함됩니다. 당신이 유의할 때, 유한 변수보다 많은 변수가 필요할 수 있습니다. 그러나 무수히 많은 무한 성이 요구되기 때문에 더 많은 것을 허용해야하는 이유는 무엇입니까?
무수한 것의 수집품은 대개 uncomputable elements 인 것 같습니다. 확실하지 않습니다. 모두 무수한 컬렉션에이 속성이 있지만 강력하게 의심됩니다.
결과적으로 합리적인 방법으로 해당 요소의 이름을 쓸 수 없습니다. 예를 들어, pi와 같은 숫자와 달리 Chaitin's constant 자릿수의 특정 유한 번호를 쓰는 프로그램을 작성할 수는 없습니다. 계산할 수있는 실수의 수는 무한대이므로, "추가적으로"얻는 것은 계산할 수 없습니다.
나는 또한 당신이 무한한 무한한 세트에서 아무것도 얻지 못한다고 생각합니다. 그래서 당신은 유익없이 (내가 볼 수있는 한) 계산할 수없는 이름을 소개 할 것입니다.
변수 가산 수 및 그들과 ℕ 사이 계산 가능한 전단 사 함수을 갖는 우리 Λ와 ℕ 사이의 전단 사 함수를 만들 수 :
표기 ⌜L ⌝는 L의 암호를 나타내는 교회 숫자 인 c _ {# L}을 나타낸다. 모든 집합 S에 대해 #S는 집합 {#L | L ∈ S}이다.
이는 람다 계산법을 증명하기 위해 decidable 우리를하지 않습니다 수 있습니다 :
이은 (A가 아닌 사소한 (안 ∅ 또는 Λ) α에 따라 폐쇄 세트와 β 평등하자 L ∈ A와 L 경우 β = M, M ∈ A). B를 집합 {L | L⌜L⌝ ∈ A}. 집합 #A가 recursive이라고 가정합니다. 그러면 f (x ∈ A이면 f (x) = 1, x ≤ A이면 0)은 μ-recursive function이어야합니다.모든 μ 재귀 함수가 정의 된 λ *이므로위한 F이 여야
F⌜L⌝ = c_1과 ⇔ ⌜L⌝ ∈
F⌜L⌝ = c_0 ⇔ ⌜L⌝ ∉
G ≡ λn. M_0은 B의 임의의 λ 항이고 M_1은 B에없는 임의의 λ 항입니다. #n은 계산 가능하므로 λ 정의가 가능합니다.
이제 "B가 G⌜G Is입니까?"라는 질문을하십시오. 그렇다면 G⌜G⌝ = M_1 ∉ B이므로 G⌜G⌝는 B에 없었을 것입니다 (B는 β =로 닫혀 있음을 기억하십시오). 그렇지 않다면 G⌜G⌝ = M_0 ∈ B이므로 B에 있어야합니다.
이것은 모순입니다. 따라서 A는 재귀 적이 될 수 없으므로 closed-under-β = non-trivial 집합이 아닙니다. 재귀 적입니다.
{L | L β = true}가 β = 및 사소하지 않은 경우 닫히므로 재귀 적이 아닙니다. 이것은 람다 미적분학이 결정할 수 없다는 것을 의미합니다.
* 증명 모든 계산 가능한 함수 (우리는 λ 기간 F되도록 F의 C_ {N1} C_ {N2} ... = C_ {F (N1, N2를 가질 수 λ가 정의 할 수 있음을, ...)})뿐만 아니라이 대답의 증거는 "Lambda Calculi With Types" by Henk Barendregt (섹션 2.2)에서 찾을 수 있습니다.