Proving compositions

If, for example, I have three functions (X a), (Y b), (Z c); and suppose that each has been complied and proven correct somehow. Now if I compose the three functions (X (Y (Z c))) is the answer proven also given the types match. I remember a paper posted on the home page that seemed to prove this, but can't seem to find it.

Comment viewing options

Select your preferred way to display the comments and click "Save settings" to activate your changes.

What is proven?

What does it mean to say it is "proven correct somehow"? Do you mean the functions are each proven to be total (ie. they terminate, returning a result value on all appropriately typed inputs)? If so, you generally need to know that the types match, and you need some guarantee that the PL handles function calls in a sane manner (eg. that it respects a CBV calling convention).

I don't know which paper you might mean.

darn, you got first post :-) (EOM)



If those three functions are proved correct "somehow" then I'm sure their composition is as well. I'm also sure the opposite is true. Ask a real question.

Civility please

Ask a real question.

He asked a "real" question, even if one thinks that it's obvious or irrelevant, so please refrain from using such harsh tones, it's against our policies here.


Didn't sound harsh to me when I wrote it but I take your point.

Anyway, you're wrong

Being "sure" about something isn't good enough. Of course one would like to assume that function composition preserves semantics. But how do we know for sure? This is a property that might or might not hold for a particular language and implementation. What would it take to be really sure? Should we really just take it as an axiom? Many equally obvious transformations hide serious problems.


I am certain that the original question was formed sufficiently ambiguous that it amounts to a rorschache test (i.e., an accidental or otherwise "troll"). I tried to point that out with "flourish" but instead came off as obnoxious. My bad.

It is a confusing question.

It is a confusing question. I was also aware of that. But why is it confusing? That is interesting also. Perhaps in software we need to think about semantics more than we are accustomed to in other areas.

It's confusing because you

It's confusing because you don't specify what you mean by "correctness" of the components nor what it "correctness" of the composition means. Your question is dramatically underspecified. It's well understood in software engineering that you can only speak of correctness with respect to some specification. Something isn't correct or incorrect on it's own. A correct implementation of a sorting algorithm is an incorrect implementation of string concatenation. Their composite is only correct if it produces the desired behaviour. Even if the components fail to meet their specifications (are "incorrect") their composite may still meet it's specification. Thus, the correctness of a composite (in this sense) neither is determined by nor determines the correctness of the components.

Using more general (partial) specifications such as memory safety or type safety, these questions can't be answered without a semantics, but usually are answered (when they are considered at all) given a semantics.


Certainly specification is very important but I would add that specification and semantics can be closely related. In the ASM method we can specify a sorting algorithm but the result is actually a semantics. This is because the ASM codes, which are not necessarily executable, are in terms of a "ground model" which is a "first order algebraic structure". We could get to an executable by "refining" the ground model "isomorphically". The system and it's correct use by following the axioms is guaranteed to produce a consistent semantics satisfying the original "specification".

Also specification can imply more than execution semantics, and there is an issue of how one translates specifications which could be economic or cultural into code.

Lastly, I am not recommending any of this but currently just trying to learn more.

Fast and Loose Reasoning is

Fast and Loose Reasoning is Morally Correct is related to your question, perhaps it's what you were looking for.

Interesting paper.

Interesting paper. Functional systems, languages, actually do have many interesting modeling interpretations because they look a lot like final systems as in systems theory. The morphism from a system with explicit state to a functional system is final (or close at least) From a modeling point of view deconstruction is also interesting.


This is really a question about common sense. We pull "things" out of the air and compose them all the time. We do it when we design things like programs, when we converse, or simply make decisions. It is common sense because even though we do it all the time we don't think about how we do it, and probably couldn't explain it if we did. How do we know that these three abstractions go together in a particular situation? My guess it that we recognize that they are on the same abstraction level (somehow) and have enough confidence that we are willing to take responsibility for composing them.

I think it is closely related to some recent posts like ASM's and abstract interpretation, also modeling in general such as model driven architecture, or model driven design. Typically if we can put the "things" into a consistent semantics we are on solid ground. But I wonder if this can be formalized or if it must remain an art?

Perlis' response

Typically if we can put the "things" into a consistent semantics we are on solid ground.

Right. A major point of formal semantics is to provide provable guarantees about things like compositionality.

(Although I'll note that re the original question, a semantics doesn't necessarily "prove correctness" e.g. with respect to some external specification, as others have also alluded to.)

But I wonder if this can be formalized or if it must remain an art?

Are you asking whether the process of formalizing can be formalized? The likely answer is no, or at best, only partially. There's a well-known Alan Perlis quote about this: "One can't proceed from the informal to the formal by formal means."


I only just found this, and certainly haven't reached any conclusions, but this site on X-machines certainly provides an answer to my question.

Edit: Also ASMs would seem to be close cousins to X-machines since the structure that ASMs transform is a first order algebraic structure.