gegenseitig rekursive Funktionen

sognul
Erstie
Erstie
Beiträge: 15
Registriert: 28. Sep 2009 16:02

gegenseitig rekursive Funktionen

Beitrag von sognul »

Hallo,

ich habe das Problem, dass ich keine 2 Funktionen definieren kann, die sich gegenseitig aufrufen. Dazu definiere ich die eine Funktion erst mal so, dass sie "leer" ist und nachdem ich die zweite Funktion so definiert habe, dass sie die erste Funktion aufruft, ändere ich die Erste, sodass sie auch die zweite Funktion aufruft. Verifun löscht bzw. markiert beide Prozeduren danach als "ignored". Und falls ich wieder was ändern möchte, beschwert es sich über zu wenig Stack. Wo liegt das Problem?

Danke im Voraus.

Sogol

sognul
Erstie
Erstie
Beiträge: 15
Registriert: 28. Sep 2009 16:02

Re: gegenseitig rekursive Funktionen

Beitrag von sognul »

Also, ich habe gerade in L Dokumentation gelesen, dass die gegenseitige Rekursion gar nicht unterstützt wird. Schade... :(

Christoph Walther
Dozentin/Dozent
Beiträge: 86
Registriert: 1. Nov 2005 18:51

Re: gegenseitig rekursive Funktionen

Beitrag von Christoph Walther »

sognul hat geschrieben:Also, ich habe gerade in L Dokumentation gelesen, dass die gegenseitige Rekursion gar nicht unterstützt wird. Schade... :(

Stimmt. Grund ist, daß die terminierungsanalyse und die berechnung von induktionsaxiomen bei gegenseitig rekursiv definierten funktionen recht aufwendig ist. Zwar machbar, aber dem implementierungsaufwand steht wenig nutzen gegenüber. Es gibt aber einen "trick": Oft kann man die gegenseitig rekursiv definierten prozeduren in einer einzigen prozedur zusammenfassen und mit einem zusätzlichen parameter dann jeweils den code für die gewünschte prozedur auswählen. An folgendem beispiel sollte klar werden, wie das im prinzip finktioniert:

Code: Alles auswählen

function even(x : nat) : bool <=
if ?0(x) then true else odd(pred(x)) end_if

Code: Alles auswählen

function odd(x : nat) : bool <=
if ?0(x) then false else even(pred(x)) end_if
Dies kann in VeriFun wegen gegenseitiger rekursion nicht definiert werden. Man kann aber beide prozeduren zu einer zusammenfassen:

Code: Alles auswählen

structure flag <=  EVEN, ODD  

function even-odd(x : nat, FLAG : flag) : bool <=
if ?0(x)
  then ?EVEN(FLAG)
  else if ?EVEN(FLAG) then even-odd(pred(x), ODD) else even-odd(pred(x), EVEN) end_if
end_if
Anstatt even(x) wird jetzt even-odd(x, EVEN) und anstatt odd(x) wird even-odd(x, ODD) aufgerufen.

sognul
Erstie
Erstie
Beiträge: 15
Registriert: 28. Sep 2009 16:02

Re: gegenseitig rekursive Funktionen

Beitrag von sognul »

Danke schön! Das war sehr hilfreich. :) Ohne den Flag hätte die Prozedur sehr hässlich ausgesehen.

Antworten

Zurück zu „Archiv“