5.1. Sintaxe🔗

Batalha naval é um jogo de tabuleiro de dois jogadores, no qual os jogadores têm de adivinhar em que quadrados estão os navios do oponente. O jogo pode ser jogado com uma comunicação bastante limitada entre os jogadores.

Cada jogador tem dois tabuleiros, 10 × 10. Usualmente, as colunas são identificadas por A..J e as linhas 0..9. Um tabuleiro representa a disposição dos navios do jogador e onde ele irá registrar os 'tiros' do seu oponente, o outro representa a tabuleiro do seu oponente, onde ele marca os 'tiros' que realizou, que podem acertar ou erras parte dos navios do oponente. O objetivo de cada jogador é revelar o tabuleiro do oponente, afundando todos os navios a frota adversária.

Modelar o jogo como uma linguagem L significa determinarmos quais são as sentenças válidas de nossa linguagem. Como o jogo é jogado em turnos, cada participante faz um ataque, marca a reação do oponente e depois recebe um ataque, indicando a consequência. Desta forma, a sentença A 10 representa um ataque na posição A × 10 do tabuleiro adversário. A sentença hit frigate representa uma reação a um tiro indicando ele ter atingido parte de uma fragata. A gramática a seguir captura esta idéia.

A notação ::= acima é BNF (Backus-Naur Form). Cada regra associa um não-terminal (à esquerda) a uma ou mais alternativas (à direita, separadas por |), cada alternativa uma sequência de símbolos. A gramática é o conjunto de regras que, quando aplicadas sucessivamente, geram todas as sentenças da linguagem. Se repetirmos a aplicação das regras acima para reescrever não terminais a partir de turn até só restarem terminais, obtém-se uma jogada válida, como B 2 missed. Se começarmos a partir do símbolo turn (chamado símbolo inicial), teremos uma jogada completa B 2 missed ou A 0 hit frigate.

Chamamos cada passo de reescrita de ⇒ e nele temos os vários estados intermediários para geração de uma sentença válida:

 turn ⇒ attack reaction ⇒ attack missed ⇒ ... ⇒ B 2 missed

A repetição de passos é o feixo transitivo e reflexivo que representamos por ⇒*:

turn ⇒* B 2 missed

A imlementação desta gramática em Lean é mostrada a seguir. Para cada não terminal, temos um tipo. Não terminais com mais de um regra de derivação, correspondem a tipos indutivos. Os terminais são os construtores. Para os não terminais com apenas uma derivação, como o attack, usamos uma structure.

Um Attack basicamente corresponde a uma coordenada, as colunas poderiam ter sido modeladas como as linhas, o que tornaria o design mais simples. Mas preferimos seguir o estilo de coordenadas usual, que facilita a leitura e associação de letras a colunas e números para linhas. Se Column também fosse um Fin 10 então poderíamos modelar com um par Attack : Fin 10 × Fin 10.

Uma possível extensão de nossa gramática seria representar como sentença um jogo completo entre dois jogadores.

Se agora tomarmos game como símbolo inicial, as sentenças que geramos são sequências de jogadas como no exemplo abaixo. Vejam que os parênteses só foram introduzidos para explicitar a estrutura sintática.

game ⇒* (A 0 missed) (B 3 (hit battleship)) (B 4 (sunk battleship))

Considerando esta nova gramática. Como a regra de game é recursiva, a gramática permite gerar sequências de turnos indefinitivamente. O não-terminal turn é sempre expandido de forma independente. Portanto, sintaticamente, nada impede que a gramática gere uma sequência de turnos onde um jogador é derrotado e o jogo continua depois disso.

game ⇒* turn turn ⇒* (A 1 defeated) (B 2 missed)

Uma forma conveniente de formalizar em Lean esta extensão é usar o tipo List para obter naturalmente uma sequencia de Turn de qualquer comprimento.

Note que game1 não representa um jogo completo e a expressão B 2 missed pode ou não ser verdade para um determinado tabuleiro. Ou seja, só temos a sintaxe, não temos a semântica do jogo. Exigir que o jogo termine quando um dos jogadores é derrotado é também uma questão semântica. Uma regra para "não atacar duas vezes a mesma posição" vai para além da sintaxe ou semântica, refere-se a pragmática, ou como ele deve ser jogado.

A gramática revisada do exercício anterior separa um turn comum (que nunca termina o jogo) de um surrender (que só ocorre no fim), usando para isso duas categorias sintáticas distintas — reaction, que perde a alternativa "defeated", e um surrender novo. Nosso Game em Lean não faz essa separação: Turn continua com o Reaction original, de quatro construtores, e Game continua sendo List Turn sem distinguir o último turno dos demais. Uma tradução fiel da gramática revisada exigiria dois tipos — um para turn e outro para surrender — e tornaria a propriedade abaixo verdadeira por construção, sem conteúdo de prova.

Preferimos manter Game como está e formalizar a propriedade que a gramática revisada garante sintaticamente como um predicado sobre essa representação existente: uma sequência de turnos é bem-formada quando defeated — se aparecer — só aparece no último turno.

O construtor step só permite estender uma sequência bem-formada com um turno cuja reação não seja defeated — é essa condição que faz o predicado, e não o tipo Game, carregar a restrição que a gramática revisada impõe estruturalmente.

Os dois exemplos de derivação já vistos são testemunhas de que a condição extra de WellFormed é mesmo necessária: game1 (linha 113) não é bem-formado, ele termina em .sunk. O jogo (A 1 defeated) (B 2 missed) também não é bem-formado, pois a derrota aparece antes do fim.

5.2. Semântica🔗

Dar semântica a Batalha Naval exige um modelo do que existe fora da linguagem — o estado do tabuleiro — e uma regra que ligue cada expressão da sintaxe a esse estado. Um estado do jogo é um tabuleiro com a posição dos navios marcada, mais o registro das células já atacadas até aquele ponto.

Os não-terminais da gramática não carregam todos o mesmo tipo de significado. column e row são referenciais: apontam para uma célula do tabuleiro, sem dizer nada sobre o que há nela. ship é denotacional: denota um subconjunto de células do tabuleiro — as que aquele navio ocupa num estado dado. attack é operacional: seu significado é a transição de um estado do jogo para outro, registrando a posição atacada — é o que updateBattle, mais adiante, implementa. Já reaction tem valor verdade, seu significado é um predicado sobre um estado e uma posição, que vale ou não vale, sem alterar nada — é o papel de hit, missed, sunk e defeated. turn, por combinar um ataque com uma reação, tem significado composto: primeiro a transição de estado, depois a verificação sobre o estado resultante.

Um tabuleiro então é apenas uma lista de pares ordenados. E como um navio ocupa células adjacentes de uma mesma linha ou coluna, também podemos entender que cada navio é uma lista de células: um encouraçado 5 células, uma fragata 4 célula, um submarino 3 células, um contratorpedeiro 2 células.

Um estado guarda a lista de grades dos navios — uma por navio, para saber depois qual navio ocupa qual célula — e a grade dos ataques sofridos. Mas nem toda lista de grades é uma distribuição de frota aceitável: duas condições precisam valer sempre, para qualquer estado que o jogo produza.

Nenhuma célula pode ser compartilhada por dois navios — a lista de todas as células dos navios não pode ter repetição.

E cada navio, sozinho, precisa ocupar células adjacentes numa única linha ou coluna.

Note que NoClashes e ShipOK são Prop, não Bool — são afirmações sobre um estado, não computações que o jogo executa a cada turno (isso é o papel de hit/missed/sunk/defeated, na próxima seção, que calculam a reação verdadeira a cada ataque). abbrev, em vez de def, mantém as duas transparentes: o Lean já sabe decidir List.Nodup e List.IsChain quando a relação de base é decidível, e a transparência é o que deixa essas instâncias alcançarem NoClashes/ShipOK sem esforço extra — uma def opaca escondia essa busca.

Em vez de deixar as duas condições como testes externos que um estado pode ou não satisfazer, podemos exigi-las já na definição do tipo: um State só existe se vier acompanhado da prova de que sua distribuição de navios as satisfaz. É o estilo idiomático de Lean — proof-carrying data —, em que a invariante não é algo a verificar depois, é parte do que significa ser um State.

Um estado que viole alguma das duas invariantes simplesmente não tipa como State — não é um valor que o programa possa produzir e testar depois, é um erro do compilador. gapShip tem uma lacuna na coluna B, então nenhum State pode conter só esse navio: a prova de shipsOK que a structure exige não existe.

A semântica de uma reação depende do estado do jogo e da posição do último ataque. Dado um estado s, uma posição p e uma reação r, queremos dizer quando r é a reação verdadeira:

• missed é verdadeira sse não há navio nenhum na posição p;

• hit s' é verdadeira sse há algum navio na posição p;

• sunk s' é verdadeira sse há um navio do tipo s' na posição p cujas células estão todas marcadas como atacadas, exceto p;

• defeated é verdadeira sse todo navio do estado está com todas as suas células marcadas.

Registrar um novo ataque só acrescenta a posição atacada à grade de ataques — o estado dos navios não muda.

5.3. Pragmática🔗

As definições da seção anterior para hit, missed, defeated e sunk seguem uma hierarquia entre as reações: todo ataque que termina uma partida (defeated) também é um ataque de afundamento (sunk), e todo ataque de afundamento também é um acerto (hit). Segue daí que a regra de jogo "reaja corretamente a um ataque" não determina, por si só, a reação apropriada em todos os casos. Pode haver mais de uma reação verdadeira ao mesmo tempo. Escolher entre elas não é questão de semântica — a semântica só diz quais reações são verdadeiras, não qual delas devemos usar. Regras de jogo desse tipo são assunto de pragmática.

H. P. Grice  (Grice, 1975)H. Paul Grice (1975). “Logic and Conversation”. Syntax and Semantics, Vol. 3: Speech Acts (P. Cole e J. Morgan, eds.), Academic Press, p. 41–58. 3., filósofo da linguagem, tratou desse tema de forma sistemática. O princípio de cooperação entre interlocutores. Grice organiza esse ajuste em máximas:

• Quantidade: Diga apenas o necessário. Não forneça menos informação do que o pedido, nem exagere com detalhes inúteis.

• Qualidade: Diga a verdade. Não afirme nada que você saiba ser falso ou que não tenha provas.

• Relação (ou Relevância): Seja pertinente. Fale apenas sobre o que importa para o momento da conversa.

• Modo (ou Maneira): Seja claro. Evite ambiguidades, termos obscuros e desordem, procurando ser breve e direto.

Como todo estímulo ao bom comportamento, as máximas são vagas, se sobrepõem, e falam em termos de verdade e informação, noções semânticas. Pragmática, nesse sentido, pressupõe semântica.

Por mais vagas que sejam, as máximas de Grice se aplicam com precisão a Batalha Naval, porque a semântica do jogo dá uma medida exata de informação. Por que sunk (quando verdadeira) é mais informativa que hit (também verdadeira na mesma situação)? Porque sunk vale para um conjunto estritamente menor de estados do jogo. O mesmo vale entre defeated e sunk. Do princípio de cooperação, dado o objetivo de deixar o oponente saber onde ele está, segue que, numa situação em que sunk vale, reagir com hit é inapropriado; a máxima de quantidade sustenta a mesma conclusão por outro caminho, exigindo a reação mais informativa em cada estágio do jogo.