🚀 go-pugleaf

In article <15341@dime.cs.umass.edu> pop@cs.umass.edu () writes:
>
>	I think it might be enlightening to talk about
>	a very small example of a formal system, namely
>	propositional logic, and then try to relate this
>	to the more complex functional systems.

These words of yours are key to the debate between
the typed-lambda-calculus /denotational-semantics approach
and the term-rewriting (equational logic) approach
to functional programming:

>	Term rewriting systems are normally first-order
>	- no function variables are permitted.
>	Thus only some functional programs using patterns
>	could actually be treated with them.
>	Some of the associated theory of term rewriting systems
>	(e.g. Knuth-Bendix) is heavily dependent
>	on the unification algorithm, which is first-order.
>	I understand that Sorted Universal Algebras
>	also provide only a first-order system.
>	Thus a more general approach would seem to be called for.

Until now, I have argued the necessity of
the denotational-semantics-based approach
for higher-order functional programming.
Now me say a word for the opposition.

Because higher-order functions are so easily
simulated in first-order functional programming,
and because equational logic is so much simpler
than the denotational approach, many argue that
higher-order capabilities are both unnecessary and undesirable
(except as syntactic sugars in a semantically 1st-order system).

This is a valid point of view.
Many decisions in programming language design
involve a trade-off between simplicity and expressisiveness.
Good work may maximize expressiveness
for a given complexity tolerance, or, alternatively,
minimize complexity to meet a given standard of expressiveness.

	Frank Silbermann	fs@rex.cs.tulane.edu