Freeciv requirements and formal logic

[sveinung]

Freeciv rule set concepts can be translated to formal logic. Formal logic can easily be transformed using the laws of logic or using software that use them. This is useful when you need to convert a rule set since it allow you to express the rules that Freeciv understands can be transformed into another way of expressing the rules that Freeciv understands via something Freeciv don't understands.

Based on Murphy's law I'm sure that this post about logic contains logical mistakes.

Introduction to logic
A statement can be true or false. Examples of statements are

Code: Select all

Socrates is a man

and

Code: Select all

"MinSize", "2", "City"

. A statement can be named.

Code: Select all

X = "MinSize", "2", "City"

is a way of saying that when you see

Code: Select all

X

think

Code: Select all

"MinSize", "2", "City"

. Just like you can add and multiply numbers you can create new statements from existing statements.

Code: Select all

X = Y && Z

is a way of saying that X is true if both X and Y are true. If one of them or both are false X is false too.

Code: Select all

X = Y || Z

is a way of saying that X is true if one of Y or Z are true. If both Y and Z are true X is true too.

Code: Select all

X = !Y

is a way of saying that X is true if Y is false and false if Y is true.

Simple requirements
The Freeciv requirement vector

Code: Select all

    { "type",   "name", "range"
      "DiplRel", "War", "Local"
      "UnitFlag", "Spy", "Local"
    }

translated to logic is

Code: Select all

("DiplRel", "War", "Local") && ("UnitFlag", "Spy", "Local")

since both must be true for the requirement vector to be true.
The requirement vector

Code: Select all

    { "type",   "name", "range", "present"
      "DiplRel", "War", "Local", TRUE
      "UnitFlag", "Spy", "Local", FALSE
    }

is

Code: Select all

("DiplRel", "War", "Local") && !("UnitFlag", "Spy", "Local")

A Freeciv requirement vector in it self can only represent && (and) and ! (not).

More than one requirement vector
Some effect typed only care if their value is above 0 or not. Unless the rule set author have used negative numbers as effect values translating an effect like that to logic is simple. Say that there are two effects of the same type. The requirement vector of the first is

Code: Select all

    { "type", "name", "range"
      "Gov", "Republic", "Player"
    }

and the requirement vector of the second is

Code: Select all

    { "type", "name", "range", "present"
      "Gov", "Democracy", "Player", TRUE
      "DiplRel", "War", "Local", FALSE
    }

. Since the effect will be triggered as long as one of them is true their translation to logic is

Code: Select all

("Gov", "Republic", "Player") || (("Gov", "Democracy", "Player") && !("DiplRel", "War", "Local"))

If the rule set autor did use negative numbers more math is required to translate the effect.

How to use this for conversion
An effect, let us call it No_Incite, makes it impossible to incide a city to change side. The action enabler "Incite City" has target requirements that test if a city can be incited. The goal is to make the action enabler behave like the effect.

The first step is to transform all No_Incite effects to logic. Say that there are two effects that both have exactly one requirement. The requirement of the first effect is Republic. The requirement of the second is Democracy. The result is

Code: Select all

No_Incite = ("Gov", "Republic", "Player") || ("Gov", "Democracy", "Player")

.

The second step is to translate the action enabler to formal logic. Since this effect was about the target city and not the attacker only the target requirement vector need translation. Say it is

Code: Select all

    { "type",   "name", "range", "present"
      "DiplRel", "Alliance", "Local", FALSE
      "DiplRel", "Team", "Local", FALSE
    }

. In logic that is

Code: Select all

target = (!("DiplRel", "Alliance", "Local") && !("DiplRel", "Team", "Local", FALSE))

The third step is to combine them. Remember that the target requirement on the action enabler is to enable the action while the requirements on the effect is to disable it. The action can be done if it isn't true that the effect is active. In logic this is

Code: Select all

merged_target = target && !No_Incite

.

The final step is to convert everything back to something Freeciv understands. I will here do it by hand.

Code: Select all

merged_target = target && !No_Incite

Insert the statements of the names target and No_Incite:

Code: Select all

merged_target = (!("DiplRel", "Alliance", "Local") && !("DiplRel", "Team", "Local", FALSE)) && !(("Gov", "Republic", "Player") || ("Gov", "Democracy", "Player"))

In logic (A && B) && C is the same as A && B && C:

Code: Select all

merged_target = !("DiplRel", "Alliance", "Local") && !("DiplRel", "Team", "Local", FALSE) && !(("Gov", "Republic", "Player") || ("Gov", "Democracy", "Player"))

!(A || B) is the same as !A && !B:

Code: Select all

merged_target = !("DiplRel", "Alliance", "Local") && !("DiplRel", "Team", "Local", FALSE) && !("Gov", "Republic", "Player") && !("Gov", "Democracy", "Player")

Since only && (and) and ! (not) is used here this can be translated to the requirement vector:

Code: Select all

    { "type",   "name", "range", "present"
      "DiplRel", "Alliance", "Local", FALSE
      "DiplRel", "Team", "Local", FALSE
      "Gov", "Democracy", "Player", FALSE
      "Gov", "Republic", "Player", FALSE
    }

Had there been an || (or) in the end result, something that more than one requirement in the vector for an effect of the No_incite type would cause, one action enabler wouldn't have been enough.