나는이사벨 함수에 적어도 하나의 인수가 있어야하는 이유는 무엇입니까?
fun foo :: "nat ⇒ nat"
where "foo = Suc"
이사벨은 "함수는 인수가 없다"고 불만을 작성하려고합니다. 왜 이런거야? 인수가없는 fun의 문제점은 무엇입니까? fun을 abbreviation 또는 definition으로 변경할 수 있으며 모두 정상입니다. 그러나 모든 다른 정의가 fun으로 선언 된 나의 .thy 파일의 균일 성을 망쳐 놓는 것은 수치 스럽습니다.
Isabelle/HOL에있는 fun 및 function의 현재 생성자 인 Alex Krauss는 이에 대한 특별한 의견을 갖고 있었으며 "함수"에 실제로 인수가 필요하다고 말하는 좋은 공식적인 이유가있을 수도 있습니다. SML에서는 실제로 비슷한 상황이 있습니다. 인수가없는 상수는 val이 아니고 fun으로 정의됩니다. 제로 인수 기능은 이자벨에 필요한 드문 상황에서
은/HOL, 떨어져 내부적으로 생성 된 키 정리의 이름에서, 대부분 동일한 결과를 얻을 수 definition [simp] "c = t를 사용하는 것이 충분히 간단하다 c.simps 대 c_def.
function의 주요 불편하고 간혹 pitfal 애플리케이션에서 사용되는 것은 아니다 보조
c_def의 그 노출 생각 :이 함수 지정 뒤에 내부 구성하지 주요 특징적 식을 전개.
ML'val' 대'fun'에 대한 연결을 그려 주셔서 감사합니다. 그것은 유용한 직관입니다. 나는 물음에 대한 나의 이유는 OCaml의 일을하는 방식에 더 끌리기 때문이라고 생각한다. 상수와 함수가 같은 키워드 인'let'을 사용하여 정의 된 것이다. –
그 외 다른 답변이 없으므로 이전 의견을 반복하여 알려주십시오.
definition (단지 이상 문에 대한 약어 역할을 상수로 볼 수있다) 비 재귀 기능 : 이자벨에서/정의 기능의 세 가지 방법이있다 HOL.
primrec (모든 재귀 호출에는 데이터 형식 생성자가 제거 된 고정 인수가 있다는 의미에서).
fun 일반적인 재귀 함수입니다.
모두, primrec 및 fun은 적어도 하나 개의 인수를 기대합니다. 전자의 경우, 인수 중 하나가 데이터 유형에 대한 원시 재귀의 구문 패턴에 해당하는지 자동으로 검사되는 반면, 후자의 경우 "종료"(또는 호출 그래프의 기초가 확실 함)를 증명하는 작업이 다음으로 위임됩니다. 어려운 경우 사용자.
어쨌든, 물론 인수없이 쉽게 경우에 definition에 primrec 및 fun을 중계 할 수있을 것이다, 그러나 적어도 나에게이 오히려 그들을 삭제하는 대신 사용자에 대한 일을 당황하게 보인다.
Chris에게 감사드립니다. 매개 변수없는'fun' 정의를'정의'메커니즘에 비밀리에 중계하는 것이 실제로 사용자를 혼란스럽게한다는 것에 동의합니다.유일하게 감지 할 수있는 행동은, 어떤 행동이 취해지면, 매개 변수없는 기능 (즉, 상수)을 허용하도록 '재미'를 확장하는 것입니다. –
'fun'는 그들의 전체 성이''primrec'와 같은 "obvios"또는''정의와 같은 사소한 것이 아니라는 의미에서 결코 사소한 기능을 위해 도입되지 않았습니다. 그러므로 call graph의 well-establishedness를 증명하는 데 사용되는 인수 (함수가 하나 이상의 인수를 취하는 경우 실제로는 튜플)가 항상 존재합니다. – chris