Qual é a base teórica da programação imperativa?

48

A programação funcional tem uma base teórica no cálculo lambda e na lógica combinatória . Como alguém envolvido com computação estatística, acho esses conceitos muito úteis para modelagem.

Existe uma base matemática equivalente de programação imperativa ou ela simplesmente surgiu da aplicação prática de hardware em linguagem de máquina e do desenvolvimento subsequente do FORTRAN ?

Shane
fonte

Respostas:

27

Em geral, quando a matemática é usada para estudar um pouco de X , primeiro é necessário um modelo de X e depois se desenvolve uma teoria, um conjunto de resultados sobre esse modelo. Eu acho que a teoria pode ser dito ser uma "base teórica" para X . Agora defina X = computação. Existem muitos modelos de computação, muitos envolvendo "estado". Cada modelo tem sua própria "teoria" e, às vezes, é possível "traduzir" entre os modelos. Acredito que seja difícil dizer qual modelo é mais "básico" - eles são simplesmente projetados com objetivos diferentes em mente.

Máquinas de Turing foram projetadas para definir o que é computável . Portanto, eles formam um bom modelo se você se importa se existe um algoritmo para um determinado problema. Às vezes, esse modelo é abusado para estudar a eficiência de algoritmos ou a dureza de problemas, sob o pretexto de que é bom o suficiente, pelo menos se você se importa apenas com polinômio / não polinomial. O modelo de RAM está mais próximo de um computador real e, portanto, melhor se você deseja uma análise precisa de um algoritmo. Para colocar limites mais baixos na dureza dos problemas, é melhor nãouse um modelo que se assemelhe demais aos computadores atuais, porque você deseja abranger uma ampla variedade de computadores possíveis, além de ser mais preciso do que apenas polinomial / não polinomial. Nesse contexto, vi, por exemplo, o modelo de célula-sonda utilizado.

Se você se preocupa com a correção , ainda outros modelos são úteis. Aqui você tem semântica operacional (que eu diria que é o análogo do cálculo lambda para cálculos estaduais completos), semântica axiomática (desenvolvida em 1969 por Hoare com base nas afirmações indutivas de Floyd de 1967, popularizadas por Knuth em The Art of Computer Programming , volume 1) e outros.

Para resumir, acho que você está atrás de modelos de computação. Existem muitos desses modelos, desenvolvidos com vários objetivos em mente, e muitos têm estado, portanto correspondem à programação imperativa. Se você quiser saber se algo pode ser calculado, consulte as máquinas de Turing. Se você se preocupa com a eficiência, consulte os modelos de RAM. Se você se preocupa com a correção, consulte modelos que terminam em "semântica", como semântica operacional.

Finalmente, deixe-me mencionar que há um grande livro on-line apenas sobre Modelos de Computação, de John Savage. É principalmente sobre eficiência. Para a parte correta, recomendo que você comece com os artigos clássicos de Floyd (1967) , Hoare (1969) , Dijkstra (1975) e Plotkin (1981) . Eles são todos bem legais.

Radu GRIGore
fonte
4
Eu acho que a Semântica Operacional é realmente o que o pôster está procurando. Um pouco mais de informação sobre a wikipedia: en.wikipedia.org/wiki/Operational_semantics
sclv
22

O modelo teórico mais simples de um programa imperativo é a própria máquina de turing. Ele possui os dois componentes essenciais de um programa imperativo: estado modificável e ilimitado e uma máquina de estado que opera nele.

Você também pode fundamentar a programação imperativa na programação funcional, considerando programas como composições de operações monádicas que passam e retornam versões modificadas do estado global, conforme feito na linguagem de programação Haskell.

Alexandre Passos
fonte
2
O uso de mônadas para obter construções do tipo imperativo em uma linguagem puramente funcional (como Haskell) não oferece todo o poder da programação imperativa. Em particular, sem um estado verdadeiramente mutável (por exemplo, como em muitas línguas com referências), ainda existem muitas estruturas de dados cuja implementação eficiente em uma linguagem puramente funcional é desconhecida.
Joshua Grochow
@ Josué: Por que você acha que as mônadas do estado não expressam a semântica das referências? Estou sem entender o que pode ser a objeção.
Charles Stewart
Uma mônada de estado é basicamente um açúcar sintático por ter uma coleção de funções que aceitam um argumento adicional (estado) e produzem uma saída adicional (próximo estado). Mas em uma linguagem puramente funcional, você não pode realmente modificar o estado para obter o próximo estado, ainda é necessário copiar e reconstruir. Não sei se existem estruturas de dados específicas nas quais se sabe que elas não podem ser implementadas eficientemente em uma linguagem puramente funcional, mas há certamente evidências sugestivas (por exemplo, Pippenger. Puro versus Impuro Lisp. 1997).
Joshua Grochow
6
Pode-se capturar perfeitamente a semântica da mutação com mônadas - veja, por exemplo, a mônada ST em Haskell. Estamos falando de semântica aqui, não de implementação.
SCLV
20

Em resumo, eu diria que a programação imperativa evoluiu da linguagem de máquina e da prática de programação. Por outro lado, as mônadas fornecem uma estrutura semântica apropriada para descrever a semântica dos recursos imperativos da linguagem de programação. O artigo Noções de computação e mônadas de Moggi estabeleceu as bases formais. Phil Wadler popularizou a idéia e contribuiu significativamente para que ela fosse a principal maneira de incorporar recursos imperativos à linguagem de programação Haskell. Trabalhos recentes de Plotkin e Power Noções de Computação Determinam Mônadas segue o caminho contrário, afirmando que algumas, mas não todas, noções de computação (imperativa) realmente dão uma mônada, o que significa que, de uma maneira muito essencial, as mônadas correspondem a noções imperativas (e outras) de computação.

Dave Clarke
fonte
8
Mônadas podem ser usadas para isolar a programação imperativa em um mundo puramente funcional, mas não vejo o argumento de afirmar que elas formam uma base teórica para a programação imperativa análoga à relação entre o cálculo lambda e muitas linguagens funcionais. As mônadas não modelam tanto a computação quanto formam uma abstração sobre as classes de computação (por exemplo, computação pura vs. computação que envolve IO ou computação que depende de um conjunto específico de estados mutáveis).
blucz 16/08/10
11
Mônadas são uma maneira de escrever semântica denotacional mais clara para linguagens eficazes, então por que não?
Noneeccop
15

Se você está procurando um tratamento matemático rigoroso de uma linguagem de programação imperativa, o livro de Winskel "A Semântica Formal de Linguagens de Programação" (1993) é um exemplo.

No livro, ele define uma linguagem de programação imperativa chamada IMP e fornece semântica operacional, denotacional e axiomática.

yhirai
fonte
14

Estou chegando tarde a essa pergunta, mas é uma pergunta fascinante. Então, aqui estão os meus pontos de vista.

Quando eu era estudante de graduação, tínhamos um ótimo professor de matemática, que costumava nos dar palestras sobre história e desenvolvimento da matemática. Segundo ele, a matemática se desenvolveu em ondas de "expansão" e "consolidação". Durante uma fase de expansão, novas idéias que antes eram desconhecidas foram consideradas e investigadas. Então, durante uma fase de consolidação, as novas teorias foram integradas ao corpo de conhecimento existente. No entanto, no século 20, ele disse, a expansão e a consolidação estão acontecendo paralelamente.

Atualmente, a programação imperativa é uma atividade de expansão para a matemática. Antes era "desconhecido". (Isso pode não ser totalmente verdade. Hoare nos diz que Euclides estava fazendo algo como programação imperativa em sua geometria. Mas a matemática perdeu o interesse nela, para melhor ou para pior.) Os matemáticos ainda não estão interessados ​​em programação imperativa. Tanto a perda para eles. Mas considero toda a Ciência da Computação um ramo da matemática em um sentido abstrato. Estamos estudando, expandindo a matemática no processo.

Portanto, eu não me importaria particularmente se existe uma base teórica a priori para a programação imperativa. Se não houver, vamos encontrá-lo. O que sabemos já nos diz que a programação imperativa é fantasticamente profunda e bonita. A programação funcional empalidece em comparação. Mas, temos muito trabalho a fazer para trazer toda essa teoria para as pessoas.

Uday Reddy
fonte
"Programação funcional empalidece em comparação". Agora, se eu pudesse colocar você e Bob Harper em uma arena de luta. Você balançaria um grande bloco de comandos e ele tentaria encerrar você. (PS: resposta muito boa, eu upvoted-lo.)
Andrej Bauer
Bem, ele meio que me evita. Eu não sei se isso significa alguma coisa :-)
Uday Reddy
11

A programação funcional tem uma base clara em matemática, porque as linguagens de programação funcional evoluíram paralelamente à matemática relevante e seus projetistas geralmente consideravam a matemática em alta consideração. O relacionamento forte e direto é uma profecia auto-realizável.

A programação imperativa tem uma história significativamente mais confusa que está muito mais ligada aos problemas de negócios e engenharia e, historicamente, estava muito mais preocupada com o desempenho dos compiladores e o código que eles geram do que com os formalismos matemáticos.

Muitas pessoas tentaram explicar a programação imperativa em termos (tradicionalmente) funcionais. Talvez seja o mais próximo possível do que você está procurando, mas essas tentativas são invariavelmente desajeitadas, tediosas e forenses. Tenho certeza de que preferiria tirar os olhos do rosto do que ler uma prova de progresso / preservação para o CLR.

Normalmente, se você chegar ao final de um livro didático pl decente (por exemplo, Tipos e Linguagens de Programação de Pierce), começará a ver a modelagem formal dos recursos imperativos da linguagem. Isso pode ser interessante para você.

blucz
fonte
11

An Axiomatic Basis for Computer Programming por CAR HOARE

Neste artigo, é feita uma tentativa de explorar os fundamentos lógicos da programação de computadores usando técnicas que foram aplicadas pela primeira vez no estudo da geometria e depois foram estendidas a outros ramos da matemática. Isso envolve a elucidação de conjuntos de axiomas e regras de inferência que podem ser usadas nas provas das propriedades dos programas de computador. São dados exemplos de tais axiomas e regras, e uma prova formal de um teorema simples é exibida. Finalmente, argumenta-se que vantagens importantes, tanto teóricas quanto práticas, podem advir da prossecução desses tópicos.

http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.85.8553&rep=rep1&type=pdf

Vag
fonte
8

Segundo o que Alexandre disse, que a máquina de Turing forneceu a base teórica original para a programação imperativa. Na medida em que a organização das linguagens de programação imperativas reflete a arquitetura da máquina, acho que o trabalho de John Von Neumann também seria uma parte fundamental de seus fundamentos teóricos.

Kurt
fonte
7

Existe uma base matemática equivalente de programação imperativa ou ela simplesmente surgiu da aplicação prática de hardware em linguagem de máquina e do desenvolvimento subsequente do FORTRAN?

Se você quer dizer "base" no sentido histórico, acho que não há "base matemática equivalente". No entanto, embora a programação imperativa tenha surgido devido a preocupações práticas, existem várias maneiras de caracterizar de forma abrangente o significado da programação imperativa de maneiras que você pode achar "útil para modelagem", como a lógica Hoare .

jbapple
fonte
você realmente quis fazer esse wiki da comunidade?
Suresh Venkat
Sim, eu pretendia torná-lo wiki da comunidade.
Jbapple
7

os posts que mencionam lógica de hoare e lógica de separação são os corretos sobre esse assunto. A lógica Hoare permite declarar propriedades de toda a configuração de heap de um programa, e a lógica de separação é o parente mais moderno que permite usar uma "conjunção de separação" que permite indicar como pré e pós condições para um segmento de código as propriedades válidas a parte do heap que o segmento de programa manipulará enquanto quantifica o restante do heap.

A resposta sobre as mônadas não é estritamente precisa, porque, em haskell, uma mônada é usada apenas porque é uma abstração que permite a codificação da ordem das restrições de avaliação e o rastreamento explícito da propriedade "poderia usar IO".

Vale ressaltar que a lógica hoare / separação pode ser vista como mônada e que existem vários projetos contemporâneos, como o ynot na harvard, que estão explorando esses tópicos.

a pesquisa em lógica de separação é um campo ativo e contínuo.

Carter Tazio Schonwald
fonte
Parece-me um erro confundir o fato de Haskell usar uma noção de mônadas (e uma classe de classe Mônada) com a abordagem mais geral, como proposto por Moggi, que usa mônadas para estruturar uma descrição da semântica categórica. A adoção de mônadas como ferramenta para estruturar a programação não deve nos cegar para o uso da semântica categórica como ferramenta para estruturar o raciocínio sobre programação.
Sclv 25/08/10
muito bom esclarecimento, embora eu acredite que muitas pessoas tenham usado mônadas à la haskell para explorar a semântica por meio de transformadores de mônada. Em particular, a semântica para diferentes operações que surgem a partir de diferentes composições dos referidos transformadores (por exemplo, para o estado / mutabilidade, continuações, não determinismo etc)
Carter Tazio Schonwald
5

Estou chegando a essa questão ainda mais tarde, mas sou igualmente fascinado por ela.

Por que a teoria da programação imperativa é considerada menos estabelecida do que a da programação funcional me escapa. Provavelmente começou a ficar sério com Scott e de Bakker em 1969, com sua análise do significado de recursão em uma linguagem imperativa simples [1]. Quando a linguagem imperativa ganha recursos, a história fica um pouco mais confusa, mas esse é apenas o preço a pagar por estar mais próximo do metal. Para citar um dos esforços mais abrangentes, em 1980, de Bakker, de Bruin e Zucker escreveram uma monografia sobre o assunto [2]. Outros foram mencionados acima. É claro que essas referências pré-datam a lógica de separação, mas [2] tratam de matrizes e procedimentos recursivos mutuamente.

[1]: inédito em 1969, mas apareceu como Jaco W. de Bakker e Dana S. Scott. Uma teoria dos programas , páginas 1-30. Em Klop et al. JW de Bakker, 25 anos atrás. CWI, Amsterdã, 1989. Liber Amoricum.

[2]: Jacobus W. de Bakker, Arie de Bruin, Jeffrey Zucker: Teoria matemática da correção do programa. Prentice Hall 1980.

Kai
fonte
11
A programação claramente imperativa é extremamente bem compreendida. Acho que o que as pessoas querem dizer quando dizem que é menos acertado é que estruturalmente, a programação imperativa é mais rica que a pura programação funcional, e muito menos estrutura matemática foi descoberta que surge nessa ou naquela forma de programação imperativa. Por exemplo, certos tipos de programas imperativos podem ser fundamentados sobre o bom uso da lógica de separação. Provavelmente isso tem a ver com formas de compartilhamento. Talvez esses tipos de programas tenham uma caracterização matemática agradável e abstrata?
Martin Berger
11
Pessoalmente, quero dizer que a teoria da modularidade em linguagens imperativas não é muito clara. Sabemos o que significa modularidade para linguagens funcionais: parametridade relacional. Para linguagens imperativas, existem muitos idiomas que escondem informações que (a) funcionam claramente, mas (b) para os quais nos faltam boas técnicas de prova. Há dicas tentadoras de que existe uma teoria profunda aqui: por exemplo, quando faço provas modulares de programas imperativos seqüenciais, acabo precisando de técnicas de simultaneidade. Informalmente, aliasing é como a simultaneidade, mas eu realmente não sei como formalizar essa ideia ...
Neel Krishnaswami
@Kai. Bem-vindo ao tópico! Já faz muito tempo desde que olhei o trabalho de De Bakker, mas acho que o problema básico é que a abordagem não foi ampliada. Para um rápido resumo do progresso da programação imperativa desde então, veja meu post no "O que constitui a semântica denotacional?" link de thread .
Uday Reddy
@NeelKrishnaswami. Eu adoraria ver essas provas. Eles estão na sua página da web? O alias é semelhante à concorrência, pois ambos envolvem compartilhamento e intercalação sofisticados. Ao mesmo tempo, você abstrai a intercalação e assume o não determinismo (o que é bom). No aliasing, você se força a lidar com a intercalação. A semântica de jogos é um excelente exemplo dessa intercalação forçada, e é por isso que não gosto disso.
Uday Reddy
3

Logo após sua pergunta, Mark Bender, da Universidade McMaster, lançou uma tese: Cálculo de atribuição: uma linguagem de raciocínio imperativo puro (8 de setembro de 2010). Esta tese descreve uma linguagem simples e imperativa correspondente ao cálculo lambda.

O cálculo de atribuição consiste em apenas quatro construções básicas, atribuição X:=t, sequência t;u, formação de ¡tprocedimento e invocação de procedimento !t. Três interpretações são dadas para AC: uma semântica operacional, uma semântica denotacional e um sistema de reescrita de termos. Os três são mostrados como equivalentes.

A tese de Mark Bender continua explorando variantes estendidas com avaliação preguiçosa, retorno e composição de procedimentos. Isso é semelhante à exploração do cálculo lambda usando pequenas extensões.

No geral, a tese fornece uma resposta relativamente direta à questão do OP.

dmbarbour
fonte
ligação pdf é quebrado
Quinn Wilson