1. That any two source programs are equal exactly when their translations are equal. So FA is parametrised by two notions of program equality, one for the source, one for the target.
2. That the source and target language are substantially different.
Requirement (2) is vague and is supposed to rule out "term models", eg. translations from a language to itself. There have been many FA results since the concept was introduced in the 1970s (I think). It's close to soundess / completenss of logic.
I mean equal w.r.t. a chosen notion of equality. So for any pair (==s, ==t) of notions of equality, there is a different notion of full abstraction. Here ==s relates programs of the source language and ==t relate programs of the target language.
1. That any two source programs are equal exactly when their translations are equal. So FA is parametrised by two notions of program equality, one for the source, one for the target.
2. That the source and target language are substantially different.
Requirement (2) is vague and is supposed to rule out "term models", eg. translations from a language to itself. There have been many FA results since the concept was introduced in the 1970s (I think). It's close to soundess / completenss of logic.