<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN">
<html>
<head>
<meta content="text/html; charset=ISO-8859-1"
http-equiv="Content-Type">
</head>
<body text="#000000" bgcolor="#ffffff">
<font size="-1"><font face="Helvetica, Arial, sans-serif">Dear Lee
Ho Yeung,<br>
<br>
The current result indicates that no counterexamples are found.<br>
In order to obtain a definition like </font></font> f x = if ( x
<= 0) 1 (x*f(x-1) you need:<br>
- a proper definition of the type Fun<br>
- define or derive an instance of the generic functions for
generation (ggen), equivalnece (gEq) en showing (genShow) elemen<font
size="-1"><font face="Helvetica, Arial, sans-serif">t of the types
used. Here you obviously need a special instance of genShow to
obtain the indicate function.<br>
- a definition of apply to turn elements of type Fun to the
corresponding function.<br>
<br>
<br>
</font></font>The types I used are:<br>
:: OR s t = L s | R t<br>
<br>
:: BinOp x = OpPlus x x | OpTimes x x | OpMinus x x<br>
:: Var = X<br>
:: Expr = Expr (OR (OR Var IConst) (BinOp Expr))<br>
:: FunAp = FunAp Int<br>
<br>
:: RFun = RFun TermVal Expr (OR (OR Var IConst) (BinOp (OR (OR Var
IConst) FunAp)))<br>
:: Fun = Fun (OR Expr RFun)<br>
<br>
:: TermVal = TermVal Int<br>
:: IConst = IConst Int<br>
<br>
The class apply looks like:<br>
<br>
class apply d e v :: d -> e -> v<br>
<br>
instance apply (OR x y) b c | apply x b c & apply y b c<br>
where<br>
apply (L x) = apply x<br>
apply (R y) = apply y<br>
<br>
instance apply (BinOp x) b v | apply x b v & +, -, * v<br>
where<br>
apply (OpPlus x y) = \b.apply x b + apply y b<br>
apply (OpMinus x y) = \b.apply x b - apply y b<br>
apply (OpTimes x y) = \b.apply x b * apply y b<br>
<br>
// ------------ apply for ints ------------<br>
<br>
instance apply IConst b Int where apply (IConst i) = \b.i<br>
instance apply Var Int Int where apply X = \i.i<br>
instance apply Var (x,Int) Int where apply X = \(_,i).i<br>
instance apply Expr Int Int where apply (Expr f) = apply f<br>
instance apply Expr (x,Int) Int where apply (Expr f) = \(_,i).apply
f i<br>
instance apply FunAp (Int->Int,Int) Int where apply (FunAp d) =
\(f,i).f (i-d)<br>
instance apply FunAp Int Int where apply (FunAp d) = abort "FunAp
Int Int"<br>
instance apply RFun Int Int<br>
where apply rf=:(RFun (TermVal c) t e) = f<br>
where f i = if (i<=c) (apply t i) (apply e (f,i))<br>
instance apply Fun Int Int where apply (Fun f) = apply f<br>
<br>
For data generation use something like:<br>
ggen{|TermVal|} n r = map TermVal [0..5]<br>
ggen{|FunAp|} n r = map FunAp [1..2]<br>
ggen{|IConst|} n r = map IConst [0..8]<br>
derive ggen OR, BinOp, Var, Expr, RFun, Fun<br>
<br>
printing can be done like:<br>
<br>
genShow{|OR|} fx fy sep p (L x) rest = fx sep p x rest<br>
genShow{|OR|} fx fy sep p (R y) rest = fy sep p y rest<br>
genShow{|IConst|} sep p (IConst c) rest = [toString c:rest]<br>
genShow{|BinOp|} fx sep p (OpPlus x y) rest = [if p "(" "": fx
sep True x ["+": fx sep True y [if p ")" "":rest]]]<br>
genShow{|BinOp|} fx sep p (OpMinus x y) rest = [if p "(" "": fx
sep True x ["-": fx sep True y [if p ")" "":rest]]]<br>
genShow{|BinOp|} fx sep p (OpTimes x y) rest = [if p "(" "": fx
sep True x ["*": fx sep True y [if p ")" "":rest]]]<br>
genShow{|Var|} sep p v rest = ["x":rest]<br>
genShow{|Expr|} sep p (Expr e) rest = genShow{|*|} sep
p e rest<br>
genShow{|FunAp|} sep p (FunAp i) rest = ["f (x-",toString
i,")":rest]<br>
genShow{|TermVal|} sep p (TermVal c) rest = [toString c:rest]<br>
genShow{|RFun|} sep p (RFun c t e) rest<br>
= ["if (x<=":genShow{|*|} sep False c[") ":genShow{|*|} sep True
t [" ": genShow{|*|} sep True e rest]]]<br>
genShow{|Fun|} sep p (Fun f) rest = ["f x = ":
genShow{|*|} sep False f rest]<br>
<br>
Hopefully this helps.<br>
<br>
Best regards,<br>
<br>
Pieter Koopman<br>
<br>
On 09/04/2011 12:00 PM, Lee Ho Yeung wrote:
<blockquote
cite="mid:BANLkTikC=w9D2OsFykXZ9rNBN=3qCzEV+A@mail.gmail.com"
type="cite">
<div>when i try the following, it only show passed after 1000 test
one case rejected and repeated with a few lines, but do not show
f x = if ( x <= 0) 1 (x*f(x-1)) as paper systematic synthesis
of functions</div>
<div> </div>
<div>which steps do i miss? </div>
<div> </div>
<div>module martin001</div>
<div>import gast, StdEnv</div>
<div>prop1 :: Fun -> Bool<br>
prop1 d = ~(f 2 == 2 && f 4 == 24 && f 6 == 720)
where f = apply d</div>
<div>Start = test prop1</div>
<pre wrap="">
<fieldset class="mimeAttachmentHeader"></fieldset>
_______________________________________________
clean-list mailing list
<a class="moz-txt-link-abbreviated" href="mailto:clean-list@science.ru.nl">clean-list@science.ru.nl</a>
<a class="moz-txt-link-freetext" href="http://mailman.science.ru.nl/mailman/listinfo/clean-list">http://mailman.science.ru.nl/mailman/listinfo/clean-list</a>
</pre>
</blockquote>
</body>
</html>