> > I do want to give definitons by pattern matching. I don't want partially > defined functions. Fortunately, pattern matching and partial functions > are separable. I accept that if partial functions can be filled up with > junk, then they don't threaten the integrity of the system as a whole. > Equally, if a partial function can be filled up with junk, then it can > be made total by writing the junk explicitly. So our debate comes down > to two key issues > > (a) Is it a useful thing to allow program equations which do not arise > from case-splitting but are in any case unambiguous to have definitional > force? [I don't have strong opinions on this matter and could be > persuaded by good examples.] > (b) Is it a useful thing to provide an automatic but necessarily > incomplete procedure to fill up under-defined programs with junk? [I > don't think so, but that's just an opinion.] > > If you disagree that these are the key issues, you had better explain > why my analysis is incorrect. >
I do apologise, Conor. I thought I could respond your question through an example. The key question may be what kind of programs (or functions) can be defined by case-splitting or pattern matching? Yong