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

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 ?

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.

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.

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.

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.

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.

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ê.

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

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.

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 .

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.

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.

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.