Isabelle에서 곱셈을위한 Primtive Recursion 정의하기

Question

Isabelle을 처음 사용하고 있으며 원시적 인 재귀 함수를 정의하려고합니다. 추가로 사용해 보았지만 곱셈에 문제가 있습니다.

datatype nati = Zero | Suc nati 

primrec add :: "nati ⇒ nati ⇒ nati" where 
"add Zero n = n" | 
"add (Suc m) n = Suc(add m n)" 

primrec mult :: "nati ⇒ nati ⇒ nati" where 
"mult Suc(Zero) n = n" | 
"mult (Suc m) n = add((mult m n) m)" 

나는

형 통일이 실패 위의 코드에 대해 다음과 같은 오류가 발생합니다 : "_ ⇒ _"및 응용 프로그램에서 "NATI"

유형 오류 유형의 충돌 : 운영자하지 않는 기능 형

운영자 : 멀티 포트 백만 : NATI

피연산자 : m : NATI

아이디어가 있으십니까?

이 문제는 당신 mult 기능

Answer 1

입니다 : 그것은 다음과 같아야합니다 함수형 프로그래밍에서

primrec mult :: "nati ⇒ nati ⇒ nati" where 
    "mult Zero n = Zero" | 
    "mult (Suc m) n = add (mult m n) m" 

기능 응용 프로그램/람다 계산법은 강한 결합 동작이며 왼쪽으로 연관 : f x y 수단 '같은 것을 f은 x에 적용되고, 결과는 y '에 적용되거나, 또는 Currying에 따라 동일하게 적용됩니다. x 및 y에 적용되는 함수 f.

따라서 mult Suc(Zero) n 같은 세 개의 파라미터, 즉 Suc, Zero 및 n 촬영하는 기능을 할 것, 즉 mult Suc Zero n로서 기능 mult를 판독 할 것이다. 그건 당신에게 타입 에러를줍니다. 마찬가지로 add ((mult m n) m)은 add (mult m n m)과 동일하므로 add은 하나의 매개 변수를 취하는 함수이고 mult은 3을 취하는 함수입니다.

마지막으로이 문제를 모두 해결하면 mult 함수의 왼쪽에 비 프리미티브 패턴이 있다고 말하는 또 다른 오류가 발생합니다. Suc Zero과 같은 패턴 매치는 원시 패턴이 아니기 때문에 패턴 매치 할 수 없습니다. primrec 대신 fun을 사용하는 경우이 작업을 수행 할 수 있지만 여기에서 수행 할 작업이 아닙니다. 대신 Zero 및 Suc 사례를 처리하려고합니다 (내 해결책 참조). 당신의 정의에서 mult Zero n은 심지어 정의되지 않을 것입니다.